Theorem mp3and 1460

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  eqsupd  8923  eqinfd  8951  updjud  9365  mreexexlemd  16917  mhmlem  18221  nn0gsumfz  19106  mdetunilem3  21225  mdetunilem9  21231  axtgupdim2  26259  axtgeucl  26260  wwlksnextprop  27693  measdivcst  31485  noprefixmo  33204  btwnouttr2  33485  btwnexch2  33486  cgrsub  33508  btwnconn1lem2  33551  btwnconn1lem5  33554  btwnconn1lem6  33555  segcon2  33568  btwnoutside  33588  broutsideof3  33589  outsideoftr  33592  outsideofeq  33593  lineelsb2  33611  relowlssretop  34646  lshpkrlem6  36253  reladdrsub  39222  fmuldfeq  41871  stoweidlem5  42297  el0ldep  44528  ldepspr  44535