Theorem mp3and 1467

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  eqsupd  9362  eqinfd  9391  updjud  9848  fvf1tp  13711  mreexexlemd  17569  mhmlem  18994  nn0gsumfz  19915  mdetunilem3  22560  mdetunilem9  22566  axtgupdim2  28524  axtgeucl  28525  wwlksnextprop  29966  measdivcst  34360  btwnouttr2  36195  btwnexch2  36196  cgrsub  36218  btwnconn1lem2  36261  btwnconn1lem5  36264  btwnconn1lem6  36265  segcon2  36278  btwnoutside  36298  broutsideof3  36299  outsideoftr  36302  outsideofeq  36303  lineelsb2  36321  relowlssretop  37537  lshpkrlem6  39410  reladdrsub  42677  onsupuni  43508  omabs2  43611  modelaxreplem2  45257  fmuldfeq  45866  stoweidlem5  46286  el0ldep  48749  ldepspr  48756