Theorem mp3an2i 1355

Description: mp3an 1350 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 1337	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 411	1 |- ( ps -> 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:  mapen  6968  mapxpen  6970  en2eleq  7334  nnledivrp  9923  xsubge0  10038  iccen  10163  fldiv4lem1div2uz2  10486  frec2uzsucd  10583  seqp1g  10648  fnpfx  11168  seq3shft  11264  geolim2  11938  geoisum1c  11946  ntrivcvgap  11974  eflegeo  12127  sin01gt0  12188  cos01gt0  12189  3dvds  12290  gcdn0gt0  12414  uzwodc  12473  divgcdodd  12580  sqpweven  12612  2sqpwodd  12613  pythagtriplem4  12706  pythagtriplem11  12712  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pcfac  12788  4sqlemffi  12834  omctfn  12929  ssnnctlemct  12932  topnvalg  13198  imasmulr  13256  imasaddfnlemg  13261  gsumsplit1r  13345  gsumprval  13346  ismhm  13408  mhmex  13409  gsumfzz  13442  prdsinvlem  13555  scaffng  14186  lss1d  14260  zringinvg  14481  psrplusgg  14555  restbasg  14755  restco  14761  lmfval  14779  cnfval  14781  cnpval  14785  upxp  14859  uptx  14861  txrest  14863  xblm  15004  bdmet  15089  bdmopn  15091  reopnap  15133  cnopnap  15198  maxcncf  15202  mincncf  15203  dvidlemap  15278  dvcj  15296  plyval  15319  plysub  15340  eflt  15362  logdivlti  15468  perfectlem1  15586  perfectlem2  15587  gausslemma2dlem0i  15649  gausslemma2dlem4  15656  lgsquad2lem1  15673  lgsquad2lem2  15674  trilpolemisumle  16179