Theorem mp3and 1492

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

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

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

This theorem is used by:  eqsupd  9415  eqinfd  9444  updjud  9927  fvf1tp  13829  mreexexlemd  17706  mhmlem  19134  nn0gsumfz  20060  mdetunilem3  22782  mdetunilem9  22788  axtgupdim2  28751  axtgeucl  28752  wwlksnextprop  30272  measdivcst  34623  btwnouttr2  36522  btwnexch2  36523  cgrsub  36545  btwnconn1lem2  36588  btwnconn1lem5  36591  btwnconn1lem6  36592  segcon2  36605  btwnoutside  36625  broutsideof3  36626  outsideoftr  36629  outsideofeq  36630  lineelsb2  36648  relowlssretop  38037  lshpkrlem6  39917  reladdrsub  43174  onsupuni  43984  omabs2  44087  modelaxreplem2  45716  fmuldfeq  46327  stoweidlem5  46747  el0ldep  49274  ldepspr  49281