Theorem mp3an2i 1378

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  mapen  7031  mapxpen  7033  en2eleq  7405  nnledivrp  10000  xsubge0  10115  iccen  10240  fldiv4lem1div2uz2  10565  frec2uzsucd  10662  seqp1g  10727  fnpfx  11257  cats1fvn  11344  seq3shft  11398  geolim2  12072  geoisum1c  12080  ntrivcvgap  12108  eflegeo  12261  sin01gt0  12322  cos01gt0  12323  3dvds  12424  gcdn0gt0  12548  uzwodc  12607  divgcdodd  12714  sqpweven  12746  2sqpwodd  12747  pythagtriplem4  12840  pythagtriplem11  12846  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pcfac  12922  4sqlemffi  12968  omctfn  13063  ssnnctlemct  13066  topnvalg  13333  imasmulr  13391  imasaddfnlemg  13396  gsumsplit1r  13480  gsumprval  13481  ismhm  13543  mhmex  13544  gsumfzz  13577  prdsinvlem  13690  scaffng  14322  lss1d  14396  zringinvg  14617  psrplusgg  14691  restbasg  14891  restco  14897  lmfval  14916  cnfval  14917  cnpval  14921  upxp  14995  uptx  14997  txrest  14999  xblm  15140  bdmet  15225  bdmopn  15227  reopnap  15269  cnopnap  15334  maxcncf  15338  mincncf  15339  dvidlemap  15414  dvcj  15432  plyval  15455  plysub  15476  eflt  15498  logdivlti  15604  perfectlem1  15722  perfectlem2  15723  gausslemma2dlem0i  15785  gausslemma2dlem4  15792  lgsquad2lem1  15809  lgsquad2lem2  15810  clwwlknon  16279  trilpolemisumle  16642