Theorem mp3an2i 1383

Description: mp3an 1378 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 1365	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 415	1 |- ( ps -> 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:  mapsnend  7103  mapen  7150  mapxpen  7152  mapunen  7155  en2eleq  7553  nnledivrp  10184  xsubge0  10300  iccen  10426  fzen  10464  fldiv4lem1div2uz2  10762  frec2uzsucd  10859  seqp1g  10924  fnpfx  11471  cats1fvn  11558  seq3shft  11625  geolim2  12304  geoisum1c  12312  ntrivcvgap  12340  eflegeo  12493  sin01gt0  12554  cos01gt0  12555  3dvds  12656  gcdn0gt0  12780  uzwodc  12839  divgcdodd  12947  sqpweven  12980  2sqpwodd  12981  pythagtriplem4  13076  pythagtriplem11  13082  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pcfac  13158  4sqlemffi  13204  ballotfilemfcc  13291  ballotfilemfmpn  13292  omctfn  13392  ssnnctlemct  13395  topnvalg  13664  imasmulr  13689  imasaddfnlemg  13694  gzsumsplit1r  13774  ismhm  13827  mhmex  13828  gsumvalfi  14242  prdsinvlem  14303  scaffng  14755  lss1d  14829  zringinvg  15048  psrplusgg  15182  psrmulrg  15186  restbasg  15394  restco  15400  lmfval  15419  cnfval  15420  cnpval  15424  upxp  15498  uptx  15500  txrest  15502  xblm  15643  bdmet  15728  bdmopn  15730  reopnap  15772  cnopnap  15837  maxcncf  15841  mincncf  15842  dvidlemap  15917  dvcj  15935  plyval  15958  plysub  15979  eflt  16001  logdivlti  16111  log2tlbndlog2  16220  perfectlem1  16299  perfectlem2  16300  gausslemma2dlem0i  16381  gausslemma2dlem4  16388  lgsquad2lem1  16405  lgsquad2lem2  16406  clwwlknon  16875  trilpolemisumle  17294