Theorem mp3and 1493

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  eqsupd  9449  eqinfd  9478  updjud  10015  fvf1tp  13929  mreexexlemd  17818  mhmlem  19272  nn0gsumfz  20198  mdetunilem3  22929  mdetunilem9  22935  axtgupdim2  28933  axtgeucl  28934  wwlksnextprop  30501  measdivcst  34857  btwnouttr2  36787  btwnexch2  36788  cgrsub  36810  btwnconn1lem2  36853  btwnconn1lem5  36856  btwnconn1lem6  36857  segcon2  36870  btwnoutside  36890  broutsideof3  36891  outsideoftr  36894  outsideofeq  36895  lineelsb2  36913  relowlssretop  38287  lshpkrlem6  40173  reladdrsub  43437  onsupuni  44231  omabs2  44334  modelaxreplem2  45969  fmuldfeq  46595  stoweidlem5  47015  el0ldep  49578  ldepspr  49585