Theorem mp3and 1443

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 1108	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		mp3and.4	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
6	4, 5	mpd 15	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  eqsupd  8716  eqinfd  8744  updjud  9157  mreexexlemd  16773  mhmlem  18006  nn0gsumfz  18854  mdetunilem3  20927  mdetunilem9  20933  axtgupdim2  25959  axtgeucl  25960  wwlksnextprop  27415  wwlksnextpropOLD  27416  measdivcst  31126  noprefixmo  32720  btwnouttr2  33001  btwnexch2  33002  cgrsub  33024  btwnconn1lem2  33067  btwnconn1lem5  33070  btwnconn1lem6  33071  segcon2  33084  btwnoutside  33104  broutsideof3  33105  outsideoftr  33108  outsideofeq  33109  lineelsb2  33127  relowlssretop  34083  lshpkrlem6  35693  reladdrsub  38645  fmuldfeq  41293  stoweidlem5  41719  el0ldep  43886  ldepspr  43893