Theorem mp3an12i 1576

Description: mp3an 1572 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an12i.1	⊢ 𝜑
mp3an12i.2	⊢ 𝜓
mp3an12i.3	⊢ (𝜒 → 𝜃)
mp3an12i.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an12i	⊢ (𝜒 → 𝜏)

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1562	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	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:  ener  8160  dfac2b  9157  hashfun  13426  funcnvs2  13867  3dvds  15261  oddp1d2  15290  bitsres  15403  pilem3  24427  bposlem9  25238  gausslemma2dlem1  25312  umgr2v2e  26656  clwlkclwwlken  27162  clwwlken  27208  0wlkonlem2  27299  clwwlknonclwlknonen  27552  dlwwlknondlwlknonen  27557  eulerpartlemgvv  30778  scutbdaybnd  32258  scutbdaylt  32259  poimirlem26  33768  mblfinlem2  33780  isosctrlem1ALT  39692  fmtnorec1  41974  evengpoap3  42212