Theorem mp3and 1427

Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)

Hypotheses

Ref	Expression
mp3and.1	⊢ (𝜑 → 𝜓)
mp3and.2	⊢ (𝜑 → 𝜒)
mp3and.3	⊢ (𝜑 → 𝜃)
mp3and.4	⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
mp3and	⊢ (𝜑 → 𝜏)

Proof of Theorem mp3and

Step	Hyp	Ref	Expression
1		mp3and.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mp3and.2	. . 3 ⊢ (𝜑 → 𝜒)
3		mp3and.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1242	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		mp3and.4	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
6	4, 5	mpd 15	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  eqsupd  8363  eqinfd  8391  mreexexlemd  16304  mhmlem  17535  nn0gsumfz  18380  mdetunilem3  20420  mdetunilem9  20426  axtgeucl  25371  wwlksnextprop  26807  measdivcst  30288  noprefixmo  31848  btwnouttr2  32129  btwnexch2  32130  cgrsub  32152  btwnconn1lem2  32195  btwnconn1lem5  32198  btwnconn1lem6  32199  segcon2  32212  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsideofeq  32237  lineelsb2  32255  relowlssretop  33211  lshpkrlem6  34402  fmuldfeq  39815  stoweidlem5  40222  el0ldep  42255  ldepspr  42262