Theorem mp3and 1465

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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  eqsupd  9452  eqinfd  9480  updjud  9929  mreexexlemd  17588  mhmlem  18945  nn0gsumfz  19852  mdetunilem3  22116  mdetunilem9  22122  axtgupdim2  27753  axtgeucl  27754  wwlksnextprop  29197  measdivcst  33253  btwnouttr2  35025  btwnexch2  35026  cgrsub  35048  btwnconn1lem2  35091  btwnconn1lem5  35094  btwnconn1lem6  35095  segcon2  35108  btwnoutside  35128  broutsideof3  35129  outsideoftr  35132  outsideofeq  35133  lineelsb2  35151  relowlssretop  36292  lshpkrlem6  38033  reladdrsub  41306  onsupuni  42026  omabs2  42130  fmuldfeq  44347  stoweidlem5  44769  el0ldep  47195  ldepspr  47202