Theorem mp3and 1494

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  9473  eqinfd  9502  updjud  10039  fvf1tp  13953  mreexexlemd  17844  mhmlem  19298  nn0gsumfz  20225  mdetunilem3  22956  mdetunilem9  22962  axtgupdim2  28960  axtgeucl  28961  wwlksnextprop  30528  measdivcst  34924  btwnouttr2  36964  btwnexch2  36965  cgrsub  36987  btwnconn1lem2  37030  btwnconn1lem5  37033  btwnconn1lem6  37034  segcon2  37047  btwnoutside  37067  broutsideof3  37068  outsideoftr  37071  outsideofeq  37072  lineelsb2  37090  relowlssretop  38477  lshpkrlem6  40363  reladdrsub  43627  onsupuni  44421  omabs2  44524  modelaxreplem2  46162  fmuldfeq  46798  stoweidlem5  47218  el0ldep  49781  ldepspr  49788