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  7032  mapxpen  7034  en2eleq  7406  nnledivrp  10001  xsubge0  10116  iccen  10241  fldiv4lem1div2uz2  10567  frec2uzsucd  10664  seqp1g  10729  fnpfx  11262  cats1fvn  11349  seq3shft  11416  geolim2  12091  geoisum1c  12099  ntrivcvgap  12127  eflegeo  12280  sin01gt0  12341  cos01gt0  12342  3dvds  12443  gcdn0gt0  12567  uzwodc  12626  divgcdodd  12733  sqpweven  12765  2sqpwodd  12766  pythagtriplem4  12859  pythagtriplem11  12865  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pcfac  12941  4sqlemffi  12987  omctfn  13082  ssnnctlemct  13085  topnvalg  13352  imasmulr  13410  imasaddfnlemg  13415  gsumsplit1r  13499  gsumprval  13500  ismhm  13562  mhmex  13563  gsumfzz  13596  prdsinvlem  13709  scaffng  14342  lss1d  14416  zringinvg  14637  psrplusgg  14711  restbasg  14911  restco  14917  lmfval  14936  cnfval  14937  cnpval  14941  upxp  15015  uptx  15017  txrest  15019  xblm  15160  bdmet  15245  bdmopn  15247  reopnap  15289  cnopnap  15354  maxcncf  15358  mincncf  15359  dvidlemap  15434  dvcj  15452  plyval  15475  plysub  15496  eflt  15518  logdivlti  15624  perfectlem1  15742  perfectlem2  15743  gausslemma2dlem0i  15805  gausslemma2dlem4  15812  lgsquad2lem1  15829  lgsquad2lem2  15830  clwwlknon  16299  trilpolemisumle  16693