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:  mapen  7075  mapxpen  7077  en2eleq  7466  nnledivrp  10062  xsubge0  10177  iccen  10303  fldiv4lem1div2uz2  10629  frec2uzsucd  10726  seqp1g  10791  fnpfx  11324  cats1fvn  11411  seq3shft  11478  geolim2  12153  geoisum1c  12161  ntrivcvgap  12189  eflegeo  12342  sin01gt0  12403  cos01gt0  12404  3dvds  12505  gcdn0gt0  12629  uzwodc  12688  divgcdodd  12795  sqpweven  12827  2sqpwodd  12828  pythagtriplem4  12921  pythagtriplem11  12927  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pcfac  13003  4sqlemffi  13049  omctfn  13144  ssnnctlemct  13147  topnvalg  13414  imasmulr  13472  imasaddfnlemg  13477  gsumsplit1r  13561  gsumprval  13562  ismhm  13624  mhmex  13625  gsumfzz  13658  prdsinvlem  13771  scaffng  14405  lss1d  14479  zringinvg  14700  psrplusgg  14779  restbasg  14979  restco  14985  lmfval  15004  cnfval  15005  cnpval  15009  upxp  15083  uptx  15085  txrest  15087  xblm  15228  bdmet  15313  bdmopn  15315  reopnap  15357  cnopnap  15422  maxcncf  15426  mincncf  15427  dvidlemap  15502  dvcj  15520  plyval  15543  plysub  15564  eflt  15586  logdivlti  15692  perfectlem1  15813  perfectlem2  15814  gausslemma2dlem0i  15876  gausslemma2dlem4  15883  lgsquad2lem1  15900  lgsquad2lem2  15901  clwwlknon  16370  trilpolemisumle  16770