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  7065  mapen  7112  mapxpen  7114  mapunen  7117  en2eleq  7511  nnledivrp  10117  xsubge0  10233  iccen  10359  fzen  10397  fldiv4lem1div2uz2  10690  frec2uzsucd  10787  seqp1g  10852  fnpfx  11394  cats1fvn  11481  seq3shft  11548  geolim2  12223  geoisum1c  12231  ntrivcvgap  12259  eflegeo  12412  sin01gt0  12473  cos01gt0  12474  3dvds  12575  gcdn0gt0  12699  uzwodc  12758  divgcdodd  12865  sqpweven  12897  2sqpwodd  12898  pythagtriplem4  12991  pythagtriplem11  12997  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pcfac  13073  4sqlemffi  13119  ballotfilemfcc  13177  ballotfilemfmpn  13178  omctfn  13278  ssnnctlemct  13281  topnvalg  13548  imasmulr  13573  imasaddfnlemg  13578  gsumsplit1r  13661  gsumprval  13662  ismhm  13716  mhmex  13717  gsumfzz  13750  prdsinvlem  14138  scaffng  14583  lss1d  14657  zringinvg  14878  psrplusgg  14959  restbasg  15159  restco  15165  lmfval  15184  cnfval  15185  cnpval  15189  upxp  15263  uptx  15265  txrest  15267  xblm  15408  bdmet  15493  bdmopn  15495  reopnap  15537  cnopnap  15602  maxcncf  15606  mincncf  15607  dvidlemap  15682  dvcj  15700  plyval  15723  plysub  15744  eflt  15766  logdivlti  15872  perfectlem1  15993  perfectlem2  15994  gausslemma2dlem0i  16056  gausslemma2dlem4  16063  lgsquad2lem1  16080  lgsquad2lem2  16081  clwwlknon  16550  trilpolemisumle  16948