Theorem mp3and 1490

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  eqsupd  9413  eqinfd  9442  updjud  9916  fvf1tp  13818  mreexexlemd  17696  mhmlem  19124  nn0gsumfz  20050  mdetunilem3  22736  mdetunilem9  22742  axtgupdim2  28702  axtgeucl  28703  wwlksnextprop  30198  measdivcst  34555  btwnouttr2  36409  btwnexch2  36410  cgrsub  36432  btwnconn1lem2  36475  btwnconn1lem5  36478  btwnconn1lem6  36479  segcon2  36492  btwnoutside  36512  broutsideof3  36513  outsideoftr  36516  outsideofeq  36517  lineelsb2  36535  relowlssretop  37892  lshpkrlem6  39774  reladdrsub  43031  onsupuni  43843  omabs2  43946  modelaxreplem2  45575  fmuldfeq  46186  stoweidlem5  46606  el0ldep  49126  ldepspr  49133