Theorem mp3an12i 1352

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

Syntax hints:   → wi 4   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  map1  6871  exmidpw2en  6973  suplocsrlempr  7874  geo2lim  11681  fprodge0  11802  fprodge1  11804  3dvds  12029  oddp1d2  12055  bezoutlema  12166  bezoutlemb  12167  pythagtriplem1  12434  exmidunben  12643  psrelbas  14228  psraddcl  14232  ismet  14580  isxmet  14581  dvidrelem  14928  coseq0negpitopi  15072  cosq34lt1  15086  cos02pilt1  15087  logdivlti  15117  1sgm2ppw  15231  lgseisenlem1  15311  lgseisen  15315  lgsquad3  15325  m1lgs  15326