Theorem mp3and 1462

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  eqsupd  9146  eqinfd  9174  updjud  9623  mreexexlemd  17270  mhmlem  18610  nn0gsumfz  19500  mdetunilem3  21671  mdetunilem9  21677  axtgupdim2  26736  axtgeucl  26737  wwlksnextprop  28178  measdivcst  32092  btwnouttr2  34251  btwnexch2  34252  cgrsub  34274  btwnconn1lem2  34317  btwnconn1lem5  34320  btwnconn1lem6  34321  segcon2  34334  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  outsideofeq  34359  lineelsb2  34377  relowlssretop  35461  lshpkrlem6  37056  reladdrsub  40289  fmuldfeq  43014  stoweidlem5  43436  el0ldep  45695  ldepspr  45702