Theorem mp3an2i 1383

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mapsnend  7105  mapen  7152  mapxpen  7154  mapunen  7157  en2eleq  7553  nnledivrp  10183  xsubge0  10299  iccen  10425  fzen  10463  fldiv4lem1div2uz2  10761  frec2uzsucd  10858  seqp1g  10923  fnpfx  11470  cats1fvn  11557  seq3shft  11624  geolim2  12303  geoisum1c  12311  ntrivcvgap  12339  eflegeo  12492  sin01gt0  12553  cos01gt0  12554  3dvds  12655  gcdn0gt0  12779  uzwodc  12838  divgcdodd  12946  sqpweven  12979  2sqpwodd  12980  pythagtriplem4  13075  pythagtriplem11  13081  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pcfac  13157  4sqlemffi  13203  ballotfilemfcc  13290  ballotfilemfmpn  13291  omctfn  13391  ssnnctlemct  13394  topnvalg  13663  imasmulr  13688  imasaddfnlemg  13693  gzsumsplit1r  13773  ismhm  13826  mhmex  13827  gsumvalfi  14241  prdsinvlem  14302  scaffng  14754  lss1d  14828  zringinvg  15047  psrplusgg  15191  psrmulrg  15195  restbasg  15411  restco  15417  lmfval  15436  cnfval  15437  cnpval  15441  upxp  15515  uptx  15517  txrest  15519  xblm  15660  bdmet  15745  bdmopn  15747  reopnap  15789  cnopnap  15854  maxcncf  15858  mincncf  15859  dvidlemap  15934  dvcj  15952  plyval  15975  plysub  15996  eflt  16018  logdivlti  16128  log2tlbndlog2  16237  perfectlem1  16316  perfectlem2  16317  gausslemma2dlem0i  16398  gausslemma2dlem4  16405  lgsquad2lem1  16422  lgsquad2lem2  16423  clwwlknon  16892  trilpolemisumle  17311