Theorem mp3an12i 1375

Description: mp3an 1371 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 1361	. 2 |- ( th -> ta )
6	1, 5	syl 14	1 |- ( ch -> ta )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  funopsn  5825  map1  6982  exmidpw2en  7097  suplocsrlempr  8017  geo2lim  12067  fprodge0  12188  fprodge1  12190  3dvds  12415  oddp1d2  12441  bezoutlema  12560  bezoutlemb  12561  pythagtriplem1  12828  exmidunben  13037  psrelbas  14679  psraddcl  14684  psr0cl  14685  psr0lid  14686  psrnegcl  14687  psrlinv  14688  psrgrp  14689  psr1clfi  14692  mplsubgfilemcl  14703  ismet  15058  isxmet  15059  dvidrelem  15406  coseq0negpitopi  15550  cosq34lt1  15564  cos02pilt1  15565  logdivlti  15595  1sgm2ppw  15709  lgseisenlem1  15789  lgseisen  15793  lgsquad3  15803  m1lgs  15804  2omapen  16531  pw1mapen  16533