Theorem mp3and 1575

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  eqsupd  8523  eqinfd  8551  updjud  8964  mreexexlemd  16512  mhmlem  17743  nn0gsumfz  18587  mdetunilem3  20638  mdetunilem9  20644  axtgeucl  25592  wwlksnextprop  27057  measdivcst  30628  noprefixmo  32185  btwnouttr2  32466  btwnexch2  32467  cgrsub  32489  btwnconn1lem2  32532  btwnconn1lem5  32535  btwnconn1lem6  32536  segcon2  32549  btwnoutside  32569  broutsideof3  32570  outsideoftr  32573  outsideofeq  32574  lineelsb2  32592  relowlssretop  33547  lshpkrlem6  34922  fmuldfeq  40328  stoweidlem5  40734  el0ldep  42778  ldepspr  42785