Theorem mp3an12i 1377

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  funopsn  5829  map1  6986  exmidpw2en  7103  suplocsrlempr  8026  geo2lim  12076  fprodge0  12197  fprodge1  12199  3dvds  12424  oddp1d2  12450  bezoutlema  12569  bezoutlemb  12570  pythagtriplem1  12837  exmidunben  13046  psrelbas  14688  psraddcl  14693  psr0cl  14694  psr0lid  14695  psrnegcl  14696  psrlinv  14697  psrgrp  14698  psr1clfi  14701  mplsubgfilemcl  14712  ismet  15067  isxmet  15068  dvidrelem  15415  coseq0negpitopi  15559  cosq34lt1  15573  cos02pilt1  15574  logdivlti  15604  1sgm2ppw  15718  lgseisenlem1  15798  lgseisen  15802  lgsquad3  15812  m1lgs  15813  2omapen  16595  pw1mapen  16597