Theorem mp3and 1487

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  eqsupd  9405  eqinfd  9434  updjud  9894  fvf1tp  13801  mreexexlemd  17678  mhmlem  19106  nn0gsumfz  20026  mdetunilem3  22676  mdetunilem9  22682  axtgupdim2  28642  axtgeucl  28643  wwlksnextprop  30114  measdivcst  34523  btwnouttr2  36377  btwnexch2  36378  cgrsub  36400  btwnconn1lem2  36443  btwnconn1lem5  36446  btwnconn1lem6  36447  segcon2  36460  btwnoutside  36480  broutsideof3  36481  outsideoftr  36484  outsideofeq  36485  lineelsb2  36503  relowlssretop  37862  lshpkrlem6  39744  reladdrsub  42999  onsupuni  43811  omabs2  43914  modelaxreplem2  45560  fmuldfeq  46164  stoweidlem5  46584  el0ldep  49093  ldepspr  49100