Theorem mp3an12i 1354

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  funopsn  5785  map1  6928  exmidpw2en  7035  suplocsrlempr  7955  geo2lim  11942  fprodge0  12063  fprodge1  12065  3dvds  12290  oddp1d2  12316  bezoutlema  12435  bezoutlemb  12436  pythagtriplem1  12703  exmidunben  12912  psrelbas  14552  psraddcl  14557  psr0cl  14558  psr0lid  14559  psrnegcl  14560  psrlinv  14561  psrgrp  14562  psr1clfi  14565  mplsubgfilemcl  14576  ismet  14931  isxmet  14932  dvidrelem  15279  coseq0negpitopi  15423  cosq34lt1  15437  cos02pilt1  15438  logdivlti  15468  1sgm2ppw  15582  lgseisenlem1  15662  lgseisen  15666  lgsquad3  15676  m1lgs  15677  2omapen  16133  pw1mapen  16135