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  6916  mapxpen  6918  en2eleq  7274  nnledivrp  9858  xsubge0  9973  iccen  10098  fldiv4lem1div2uz2  10413  frec2uzsucd  10510  seqp1g  10575  seq3shft  11020  geolim2  11694  geoisum1c  11702  ntrivcvgap  11730  eflegeo  11883  sin01gt0  11944  cos01gt0  11945  3dvds  12046  gcdn0gt0  12170  uzwodc  12229  divgcdodd  12336  sqpweven  12368  2sqpwodd  12369  pythagtriplem4  12462  pythagtriplem11  12468  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pcfac  12544  4sqlemffi  12590  omctfn  12685  ssnnctlemct  12688  topnvalg  12953  imasmulr  13011  imasaddfnlemg  13016  gsumsplit1r  13100  gsumprval  13101  ismhm  13163  mhmex  13164  gsumfzz  13197  prdsinvlem  13310  scaffng  13941  lss1d  14015  zringinvg  14236  psrplusgg  14306  restbasg  14488  restco  14494  lmfval  14512  cnfval  14514  cnpval  14518  upxp  14592  uptx  14594  txrest  14596  xblm  14737  bdmet  14822  bdmopn  14824  reopnap  14866  cnopnap  14931  maxcncf  14935  mincncf  14936  dvidlemap  15011  dvcj  15029  plyval  15052  plysub  15073  eflt  15095  logdivlti  15201  perfectlem1  15319  perfectlem2  15320  gausslemma2dlem0i  15382  gausslemma2dlem4  15389  lgsquad2lem1  15406  lgsquad2lem2  15407  trilpolemisumle  15769