Theorem mp3an2i 1376

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  mapen  7007  mapxpen  7009  en2eleq  7373  nnledivrp  9962  xsubge0  10077  iccen  10202  fldiv4lem1div2uz2  10526  frec2uzsucd  10623  seqp1g  10688  fnpfx  11209  cats1fvn  11296  seq3shft  11349  geolim2  12023  geoisum1c  12031  ntrivcvgap  12059  eflegeo  12212  sin01gt0  12273  cos01gt0  12274  3dvds  12375  gcdn0gt0  12499  uzwodc  12558  divgcdodd  12665  sqpweven  12697  2sqpwodd  12698  pythagtriplem4  12791  pythagtriplem11  12797  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pcfac  12873  4sqlemffi  12919  omctfn  13014  ssnnctlemct  13017  topnvalg  13284  imasmulr  13342  imasaddfnlemg  13347  gsumsplit1r  13431  gsumprval  13432  ismhm  13494  mhmex  13495  gsumfzz  13528  prdsinvlem  13641  scaffng  14273  lss1d  14347  zringinvg  14568  psrplusgg  14642  restbasg  14842  restco  14848  lmfval  14867  cnfval  14868  cnpval  14872  upxp  14946  uptx  14948  txrest  14950  xblm  15091  bdmet  15176  bdmopn  15178  reopnap  15220  cnopnap  15285  maxcncf  15289  mincncf  15290  dvidlemap  15365  dvcj  15383  plyval  15406  plysub  15427  eflt  15449  logdivlti  15555  perfectlem1  15673  perfectlem2  15674  gausslemma2dlem0i  15736  gausslemma2dlem4  15743  lgsquad2lem1  15760  lgsquad2lem2  15761  trilpolemisumle  16406