Theorem mp3and 1466

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 1128	. 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  9415  eqinfd  9444  updjud  9894  fvf1tp  13758  mreexexlemd  17612  mhmlem  19001  nn0gsumfz  19921  mdetunilem3  22508  mdetunilem9  22514  axtgupdim2  28405  axtgeucl  28406  wwlksnextprop  29849  measdivcst  34221  btwnouttr2  36017  btwnexch2  36018  cgrsub  36040  btwnconn1lem2  36083  btwnconn1lem5  36086  btwnconn1lem6  36087  segcon2  36100  btwnoutside  36120  broutsideof3  36121  outsideoftr  36124  outsideofeq  36125  lineelsb2  36143  relowlssretop  37358  lshpkrlem6  39115  reladdrsub  42380  onsupuni  43225  omabs2  43328  modelaxreplem2  44976  fmuldfeq  45588  stoweidlem5  46010  el0ldep  48459  ldepspr  48466