Theorem mp3an12i 1323

Description: mp3an 1319 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 1309	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  map1  6757  suplocsrlempr  7727  geo2lim  11413  fprodge0  11534  fprodge1  11536  oddp1d2  11780  bezoutlema  11882  bezoutlemb  11883  exmidunben  12155  ismet  12744  isxmet  12745  coseq0negpitopi  13157  cosq34lt1  13171  cos02pilt1  13172  logdivlti  13202