Theorem mp3an12i 1354

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  funopsn  5787  map1  6930  exmidpw2en  7037  suplocsrlempr  7957  geo2lim  11988  fprodge0  12109  fprodge1  12111  3dvds  12336  oddp1d2  12362  bezoutlema  12481  bezoutlemb  12482  pythagtriplem1  12749  exmidunben  12958  psrelbas  14598  psraddcl  14603  psr0cl  14604  psr0lid  14605  psrnegcl  14606  psrlinv  14607  psrgrp  14608  psr1clfi  14611  mplsubgfilemcl  14622  ismet  14977  isxmet  14978  dvidrelem  15325  coseq0negpitopi  15469  cosq34lt1  15483  cos02pilt1  15484  logdivlti  15514  1sgm2ppw  15628  lgseisenlem1  15708  lgseisen  15712  lgsquad3  15722  m1lgs  15723  2omapen  16241  pw1mapen  16243