Theorem mp3an12i 1382

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  funopsn  5894  map1  7107  exmidpw2en  7225  2omapen  7325  suplocsrlempr  8180  hashf1lem1  11306  geo2lim  12307  fprodge0  12428  fprodge1  12430  3dvds  12655  oddp1d2  12681  bezoutlema  12800  bezoutlemb  12801  pythagtriplem1  13072  exmidunben  13374  psrelbas  15188  psraddcl  15193  psrmulfval  15196  psrmulclfilem  15198  psr0cl  15200  psr0lid  15201  psrnegcl  15202  psrlinv  15203  psrgrp  15204  psr1clfi  15207  psrdifi  15211  psrdirfi  15212  mvrval  15215  mvrffi  15218  ismet  15587  isxmet  15588  dvidrelem  15935  coseq0negpitopi  16080  cosq34lt1  16095  cos02pilt1  16096  logdivlti  16128  1sgm2ppw  16306  ppiublem1  16308  bposlem6  16333  bposlem9  16336  lgseisenlem1  16411  lgseisen  16415  lgsquad3  16425  m1lgs  16426  pw1mapen  17248