Theorem mp3and 1463

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  eqsupd  9495  eqinfd  9523  updjud  9972  fvf1tp  13826  mreexexlemd  17689  mhmlem  19093  nn0gsumfz  20017  mdetunilem3  22636  mdetunilem9  22642  axtgupdim2  28494  axtgeucl  28495  wwlksnextprop  29942  measdivcst  34205  btwnouttr2  36004  btwnexch2  36005  cgrsub  36027  btwnconn1lem2  36070  btwnconn1lem5  36073  btwnconn1lem6  36074  segcon2  36087  btwnoutside  36107  broutsideof3  36108  outsideoftr  36111  outsideofeq  36112  lineelsb2  36130  relowlssretop  37346  lshpkrlem6  39097  reladdrsub  42392  onsupuni  43218  omabs2  43322  modelaxreplem2  44944  fmuldfeq  45539  stoweidlem5  45961  el0ldep  48312  ldepspr  48319