Theorem mp3and 1466

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  eqsupd  9384  eqinfd  9413  updjud  9865  fvf1tp  13729  mreexexlemd  17586  mhmlem  18977  nn0gsumfz  19899  mdetunilem3  22535  mdetunilem9  22541  axtgupdim2  28452  axtgeucl  28453  wwlksnextprop  29893  measdivcst  34208  btwnouttr2  36004  btwnexch2  36005  cgrsub  36027  btwnconn1lem2  36070  btwnconn1lem5  36073  btwnconn1lem6  36074  segcon2  36087  btwnoutside  36107  broutsideof3  36108  outsideoftr  36111  outsideofeq  36112  lineelsb2  36130  relowlssretop  37345  lshpkrlem6  39102  reladdrsub  42367  onsupuni  43212  omabs2  43315  modelaxreplem2  44963  fmuldfeq  45575  stoweidlem5  45997  el0ldep  48449  ldepspr  48456