Theorem mp3an2i 1379

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  mapsnend  7052  mapen  7099  mapxpen  7101  mapunen  7104  en2eleq  7498  nnledivrp  10099  xsubge0  10214  iccen  10340  fzen  10377  fldiv4lem1div2uz2  10666  frec2uzsucd  10763  seqp1g  10828  fnpfx  11369  cats1fvn  11456  seq3shft  11523  geolim2  12198  geoisum1c  12206  ntrivcvgap  12234  eflegeo  12387  sin01gt0  12448  cos01gt0  12449  3dvds  12550  gcdn0gt0  12674  uzwodc  12733  divgcdodd  12840  sqpweven  12872  2sqpwodd  12873  pythagtriplem4  12966  pythagtriplem11  12972  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pcfac  13048  4sqlemffi  13094  omctfn  13194  ssnnctlemct  13197  topnvalg  13464  imasmulr  13522  imasaddfnlemg  13527  gsumsplit1r  13611  gsumprval  13612  ismhm  13674  mhmex  13675  gsumfzz  13708  prdsinvlem  13821  scaffng  14457  lss1d  14531  zringinvg  14752  psrplusgg  14833  restbasg  15033  restco  15039  lmfval  15058  cnfval  15059  cnpval  15063  upxp  15137  uptx  15139  txrest  15141  xblm  15282  bdmet  15367  bdmopn  15369  reopnap  15411  cnopnap  15476  maxcncf  15480  mincncf  15481  dvidlemap  15556  dvcj  15574  plyval  15597  plysub  15618  eflt  15640  logdivlti  15746  perfectlem1  15867  perfectlem2  15868  gausslemma2dlem0i  15930  gausslemma2dlem4  15937  lgsquad2lem1  15954  lgsquad2lem2  15955  clwwlknon  16424  trilpolemisumle  16822