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  7099  mapen  7146  mapxpen  7148  mapunen  7151  en2eleq  7547  nnledivrp  10167  xsubge0  10283  iccen  10409  fzen  10447  fldiv4lem1div2uz2  10741  frec2uzsucd  10838  seqp1g  10903  fnpfx  11449  cats1fvn  11536  seq3shft  11603  geolim2  12279  geoisum1c  12287  ntrivcvgap  12315  eflegeo  12468  sin01gt0  12529  cos01gt0  12530  3dvds  12631  gcdn0gt0  12755  uzwodc  12814  divgcdodd  12921  sqpweven  12953  2sqpwodd  12954  pythagtriplem4  13047  pythagtriplem11  13053  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pcfac  13129  4sqlemffi  13175  ballotfilemfcc  13233  ballotfilemfmpn  13234  omctfn  13334  ssnnctlemct  13337  topnvalg  13605  imasmulr  13630  imasaddfnlemg  13635  gzsumsplit1r  13715  ismhm  13768  mhmex  13769  gsumvalfi  14152  prdsinvlem  14196  scaffng  14646  lss1d  14720  zringinvg  14939  psrplusgg  15069  restbasg  15269  restco  15275  lmfval  15294  cnfval  15295  cnpval  15299  upxp  15373  uptx  15375  txrest  15377  xblm  15518  bdmet  15603  bdmopn  15605  reopnap  15647  cnopnap  15712  maxcncf  15716  mincncf  15717  dvidlemap  15792  dvcj  15810  plyval  15833  plysub  15854  eflt  15876  logdivlti  15982  log2tlbndlog2  16082  perfectlem1  16113  perfectlem2  16114  gausslemma2dlem0i  16176  gausslemma2dlem4  16183  lgsquad2lem1  16200  lgsquad2lem2  16201  clwwlknon  16670  trilpolemisumle  17087