Theorem mp3and 1419

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  eqsupd  8246  eqinfd  8274  mreexexlemd  16127  mhmlem  17358  nn0gsumfz  18203  mdetunilem3  20239  mdetunilem9  20245  axtgeucl  25171  wwlkextprop  26272  measdivcst  29615  btwnouttr2  31299  btwnexch2  31300  cgrsub  31322  btwnconn1lem2  31365  btwnconn1lem5  31368  btwnconn1lem6  31369  segcon2  31382  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsideofeq  31407  lineelsb2  31425  relowlssretop  32387  lshpkrlem6  33420  fmuldfeq  38650  stoweidlem5  38898  wwlksnextprop  41118  el0ldep  42049  ldepspr  42056