Theorem mpan9 486

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	|- ( ph -> ps )
mpan9.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
mpan9	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 |- ( ph -> ps )
2		mpan9.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5 34	. 2 |- ( ch -> ( ph -> th ) )
4	3	impcom 446	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  sylan  488  vtocl2gf  3268  vtocl3gf  3269  vtoclegft  3280  sbcthdv  3451  elinsn  4245  swopolem  5044  wereu  5110  funssres  5930  dffv2  6271  fmptcof  6397  fnprb  6472  fntpb  6473  fliftfuns  6564  isorel  6576  oveqrspc2v  6673  caovclg  6826  caovcomg  6829  caovassg  6832  caovcang  6835  caovordig  6839  caovordg  6841  caovdig  6848  caovdirg  6851  peano5  7089  fvmpt2curryd  7397  qliftfuns  7834  nneneq  8143  cfslb  9088  hsmexlem4  9251  axdc3lem2  9273  axdc4lem  9277  adderpq  9778  mulerpq  9779  ltordlem  10553  lble  10975  uz11  11710  xrsupsslem  12137  xrinfmsslem  12138  xrsupss  12139  xrinfmss  12140  fseqsupubi  12777  hashbclem  13236  swrdswrd  13460  swrdccatin2  13487  cshwcsh2id  13574  wwlktovf  13699  isercolllem1  14395  caucvgb  14410  zsum  14449  fsum  14451  fsumf1o  14454  fsumcvg2  14458  isummulc2  14493  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  fsum00  14530  fsumrlim  14543  o1fsum  14545  isumshft  14571  clim2prod  14620  ntrivcvgfvn0  14631  zprod  14667  fprod  14671  fprodf1o  14676  prodss  14677  fprodser  14679  fprodm1s  14700  fprodp1s  14701  fprodabs  14704  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fprodefsum  14825  mod2eq1n2dvds  15071  sumeven  15110  lcmfun  15358  dvdsprm  15415  pythagtriplem4  15524  pcmptdvds  15598  prslem  16931  posi  16950  dlatmjdi  17194  grpidinv2  17474  ghmlin  17665  cntzmhm2  17772  dprdss  18428  dprd2d2  18443  srgrz  18526  srglz  18527  ringinvnz1ne0  18592  lmodlema  18868  islmodd  18869  lsscl  18943  lsslss  18961  lspdisjb  19126  rrgeq0i  19289  assalem  19316  lsslinds  20170  fvmptnn04if  20654  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  ssnei2  20920  t1ficld  21131  t1sep2  21173  unconn  21232  1stcclb  21247  ptbasfi  21384  tx1stc  21453  qtoptop2  21502  r0sep  21551  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  psmet0  22113  psmettri2  22114  prdsdsf  22172  prdsxmet  22174  cncfi  22697  ovolfiniun  23269  mbfimaopnlem  23422  limciun  23658  dvcn  23684  dvmptfsum  23738  dvfsumle  23784  dvfsumabs  23786  dvfsumlem3  23791  itgsubst  23812  fsumvma  24938  dchrelbasd  24964  dchrisumlem3  25180  axcontlem9  25852  usgruspgrb  26076  uspgrloopvtxel  26412  umgr2v2evtxel  26418  3spthd  27036  numclwwlkovf2exlem2  27212  grpoass  27357  lnolin  27609  elnlfn  28787  strlem4  29113  hstrlem4  29121  atmd  29258  nn0min  29567  omndadd  29706  slmdlema  29756  esumcvg  30148  measxun2  30273  sibfima  30400  bnj110  30928  bnj594  30982  bnj1491  31125  cvmcov  31245  mrsubcn  31416  dfon2lem5  31692  frrlem4  31783  sssslt1  31906  madeval2  31936  ifscgr  32151  nn0prpw  32318  neibastop2lem  32355  bj-restb  33047  poimirlem25  33434  poimirlem32  33441  mbfresfi  33456  totbndss  33576  ghomlinOLD  33687  rngodi  33703  rngodir  33704  rngoass  33705  rngohomadd  33768  rngohommul  33769  crngocom  33800  idladdcl  33818  idllmulcl  33819  idlrmulcl  33820  exlimddvf  33926  oposlem  34469  cvlexch1  34615  hlsuprexch  34667  lautle  35370  elrfirn2  37259  wepwsolem  37612  kelac1  37633  islssfg2  37641  lnmlssfg  37650  2elfz3nn0  41326  2elfz2melfz  41328  icceuelpartlem  41371  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbnd  41697  setrec2fun  42439