Theorem mp3an2i 1332

Description: mp3an 1327 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an2i.1	|- ph
mp3an2i.2	|- ( ps -> ch )
mp3an2i.3	|- ( ps -> th )
mp3an2i.4	|- ( ( ph /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
mp3an2i	|- ( ps -> ta )

Proof of Theorem mp3an2i

Step	Hyp	Ref	Expression
1		mp3an2i.2	. 2 |- ( ps -> ch )
2		mp3an2i.3	. 2 |- ( ps -> th )
3		mp3an2i.1	. . 3 |- ph
4		mp3an2i.4	. . 3 |- ( ( ph /\ ch /\ th ) -> ta )
5	3, 4	mp3an1 1314	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 409	1 |- ( ps -> ta )

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mapen  6808  mapxpen  6810  en2eleq  7147  nnledivrp  9698  xsubge0  9813  iccen  9938  frec2uzsucd  10332  seq3shft  10776  geolim2  11449  geoisum1c  11457  ntrivcvgap  11485  eflegeo  11638  sin01gt0  11698  cos01gt0  11699  gcdn0gt0  11907  uzwodc  11966  divgcdodd  12071  sqpweven  12103  2sqpwodd  12104  pythagtriplem4  12196  pythagtriplem11  12202  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pcfac  12276  omctfn  12372  ssnnctlemct  12375  ressid  12451  topnvalg  12563  restbasg  12768  restco  12774  lmfval  12792  cnfval  12794  cnpval  12798  upxp  12872  uptx  12874  txrest  12876  xblm  13017  bdmet  13102  bdmopn  13104  reopnap  13138  cnopnap  13194  dvidlemap  13260  dvcj  13273  eflt  13296  logdivlti  13402  trilpolemisumle  13877