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  9417  eqinfd  9446  updjud  9920  fvf1tp  13822  mreexexlemd  17700  mhmlem  19128  nn0gsumfz  20054  mdetunilem3  22740  mdetunilem9  22746  axtgupdim2  28706  axtgeucl  28707  wwlksnextprop  30202  measdivcst  34559  btwnouttr2  36447  btwnexch2  36448  cgrsub  36470  btwnconn1lem2  36513  btwnconn1lem5  36516  btwnconn1lem6  36517  segcon2  36530  btwnoutside  36550  broutsideof3  36551  outsideoftr  36554  outsideofeq  36555  lineelsb2  36573  relowlssretop  37932  lshpkrlem6  39814  reladdrsub  43071  onsupuni  43883  omabs2  43986  modelaxreplem2  45615  fmuldfeq  46226  stoweidlem5  46646  el0ldep  49166  ldepspr  49173