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  9408  eqinfd  9437  updjud  9887  fvf1tp  13751  mreexexlemd  17605  mhmlem  18994  nn0gsumfz  19914  mdetunilem3  22501  mdetunilem9  22507  axtgupdim2  28398  axtgeucl  28399  wwlksnextprop  29842  measdivcst  34214  btwnouttr2  36010  btwnexch2  36011  cgrsub  36033  btwnconn1lem2  36076  btwnconn1lem5  36079  btwnconn1lem6  36080  segcon2  36093  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  outsideofeq  36118  lineelsb2  36136  relowlssretop  37351  lshpkrlem6  39108  reladdrsub  42373  onsupuni  43218  omabs2  43321  modelaxreplem2  44969  fmuldfeq  45581  stoweidlem5  46003  el0ldep  48455  ldepspr  48462