Theorem mp3an12i 1382

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

Hypotheses

Ref	Expression
mp3an12i.1	|- ph
mp3an12i.2	|- ps
mp3an12i.3	|- ( ch -> th )
mp3an12i.4	|- ( ( ph /\ ps /\ th ) -> ta )

Assertion

Ref	Expression
mp3an12i	|- ( ch -> ta )

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 |- ( ch -> th )
2		mp3an12i.1	. . 3 |- ph
3		mp3an12i.2	. . 3 |- ps
4		mp3an12i.4	. . 3 |- ( ( ph /\ ps /\ th ) -> ta )
5	2, 3, 4	mp3an12 1368	. 2 |- ( th -> ta )
6	1, 5	syl 14	1 |- ( ch -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  funopsn  5894  map1  7105  exmidpw2en  7223  2omapen  7325  suplocsrlempr  8180  hashf1lem1  11307  geo2lim  12308  fprodge0  12429  fprodge1  12431  3dvds  12656  oddp1d2  12682  bezoutlema  12801  bezoutlemb  12802  pythagtriplem1  13073  exmidunben  13375  psrelbas  15179  psraddcl  15184  psrmulfval  15187  psrmulclfilem  15189  psr0cl  15191  psr0lid  15192  psrnegcl  15193  psrlinv  15194  psrgrp  15195  psr1clfi  15198  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  ismet  15570  isxmet  15571  dvidrelem  15918  coseq0negpitopi  16063  cosq34lt1  16078  cos02pilt1  16079  logdivlti  16111  1sgm2ppw  16289  ppiublem1  16291  bposlem6  16316  bposlem9  16319  lgseisenlem1  16394  lgseisen  16398  lgsquad3  16408  m1lgs  16409  pw1mapen  17231