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  5830  map1  6987  exmidpw2en  7104  suplocsrlempr  8027  geo2lim  12095  fprodge0  12216  fprodge1  12218  3dvds  12443  oddp1d2  12469  bezoutlema  12588  bezoutlemb  12589  pythagtriplem1  12856  exmidunben  13065  psrelbas  14708  psraddcl  14713  psr0cl  14714  psr0lid  14715  psrnegcl  14716  psrlinv  14717  psrgrp  14718  psr1clfi  14721  mplsubgfilemcl  14732  ismet  15087  isxmet  15088  dvidrelem  15435  coseq0negpitopi  15579  cosq34lt1  15593  cos02pilt1  15594  logdivlti  15624  1sgm2ppw  15738  lgseisenlem1  15818  lgseisen  15822  lgsquad3  15832  m1lgs  15833  2omapen  16646  pw1mapen  16648