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  9364  eqinfd  9393  updjud  9850  fvf1tp  13713  mreexexlemd  17571  mhmlem  18996  nn0gsumfz  19917  mdetunilem3  22562  mdetunilem9  22568  axtgupdim2  28547  axtgeucl  28548  wwlksnextprop  29989  measdivcst  34383  btwnouttr2  36218  btwnexch2  36219  cgrsub  36241  btwnconn1lem2  36284  btwnconn1lem5  36287  btwnconn1lem6  36288  segcon2  36301  btwnoutside  36321  broutsideof3  36322  outsideoftr  36325  outsideofeq  36326  lineelsb2  36344  relowlssretop  37570  lshpkrlem6  39443  reladdrsub  42707  onsupuni  43538  omabs2  43641  modelaxreplem2  45287  fmuldfeq  45896  stoweidlem5  46316  el0ldep  48779  ldepspr  48786