Theorem mp3an2i 1353

Description: mp3an 1348 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 1335	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 411	1 |- ( ps -> ta )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  mapen  6904  mapxpen  6906  en2eleq  7257  nnledivrp  9835  xsubge0  9950  iccen  10075  fldiv4lem1div2uz2  10378  frec2uzsucd  10475  seqp1g  10540  seq3shft  10985  geolim2  11658  geoisum1c  11666  ntrivcvgap  11694  eflegeo  11847  sin01gt0  11908  cos01gt0  11909  gcdn0gt0  12118  uzwodc  12177  divgcdodd  12284  sqpweven  12316  2sqpwodd  12317  pythagtriplem4  12409  pythagtriplem11  12415  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pcfac  12491  4sqlemffi  12537  omctfn  12603  ssnnctlemct  12606  topnvalg  12865  imasmulr  12895  imasaddfnlemg  12900  gsumsplit1r  12984  gsumprval  12985  ismhm  13036  mhmex  13037  gsumfzz  13070  scaffng  13808  lss1d  13882  zringinvg  14103  psrplusgg  14173  restbasg  14347  restco  14353  lmfval  14371  cnfval  14373  cnpval  14377  upxp  14451  uptx  14453  txrest  14455  xblm  14596  bdmet  14681  bdmopn  14683  reopnap  14725  cnopnap  14790  maxcncf  14794  mincncf  14795  dvidlemap  14870  dvcj  14888  plyval  14911  plysub  14932  eflt  14951  logdivlti  15057  gausslemma2dlem0i  15214  gausslemma2dlem4  15221  lgsquad2lem1  15238  lgsquad2lem2  15239  trilpolemisumle  15598