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  5817  map1  6965  exmidpw2en  7074  suplocsrlempr  7994  geo2lim  12027  fprodge0  12148  fprodge1  12150  3dvds  12375  oddp1d2  12401  bezoutlema  12520  bezoutlemb  12521  pythagtriplem1  12788  exmidunben  12997  psrelbas  14639  psraddcl  14644  psr0cl  14645  psr0lid  14646  psrnegcl  14647  psrlinv  14648  psrgrp  14649  psr1clfi  14652  mplsubgfilemcl  14663  ismet  15018  isxmet  15019  dvidrelem  15366  coseq0negpitopi  15510  cosq34lt1  15524  cos02pilt1  15525  logdivlti  15555  1sgm2ppw  15669  lgseisenlem1  15749  lgseisen  15753  lgsquad3  15763  m1lgs  15764  2omapen  16360  pw1mapen  16362