Theorem mp3an2i 1353

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  mapen  6902  mapxpen  6904  en2eleq  7255  nnledivrp  9832  xsubge0  9947  iccen  10072  fldiv4lem1div2uz2  10375  frec2uzsucd  10472  seqp1g  10537  seq3shft  10982  geolim2  11655  geoisum1c  11663  ntrivcvgap  11691  eflegeo  11844  sin01gt0  11905  cos01gt0  11906  gcdn0gt0  12115  uzwodc  12174  divgcdodd  12281  sqpweven  12313  2sqpwodd  12314  pythagtriplem4  12406  pythagtriplem11  12412  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pcfac  12488  4sqlemffi  12534  omctfn  12600  ssnnctlemct  12603  topnvalg  12862  imasmulr  12892  imasaddfnlemg  12897  gsumsplit1r  12981  gsumprval  12982  ismhm  13033  mhmex  13034  gsumfzz  13067  scaffng  13805  lss1d  13879  zringinvg  14092  psrplusgg  14162  restbasg  14336  restco  14342  lmfval  14360  cnfval  14362  cnpval  14366  upxp  14440  uptx  14442  txrest  14444  xblm  14585  bdmet  14670  bdmopn  14672  reopnap  14706  cnopnap  14765  maxcncf  14769  mincncf  14770  dvidlemap  14845  dvcj  14858  plyval  14878  plysub  14899  eflt  14910  logdivlti  15016  gausslemma2dlem0i  15173  gausslemma2dlem4  15180  trilpolemisumle  15528