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  5819  map1  6973  exmidpw2en  7082  suplocsrlempr  8002  geo2lim  12035  fprodge0  12156  fprodge1  12158  3dvds  12383  oddp1d2  12409  bezoutlema  12528  bezoutlemb  12529  pythagtriplem1  12796  exmidunben  13005  psrelbas  14647  psraddcl  14652  psr0cl  14653  psr0lid  14654  psrnegcl  14655  psrlinv  14656  psrgrp  14657  psr1clfi  14660  mplsubgfilemcl  14671  ismet  15026  isxmet  15027  dvidrelem  15374  coseq0negpitopi  15518  cosq34lt1  15532  cos02pilt1  15533  logdivlti  15563  1sgm2ppw  15677  lgseisenlem1  15757  lgseisen  15761  lgsquad3  15771  m1lgs  15772  2omapen  16386  pw1mapen  16388