MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan9 Structured version   Unicode version

Theorem mpan9 469
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
StepHypRef Expression
1 mpan9.1 . . 3  |-  ( ph  ->  ps )
2 mpan9.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
31, 2syl5 32 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 430 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  sylan  471  vtocl2gf  3173  vtocl3gf  3174  vtoclegft  3185  sbcthdv  3347  swopolem  4809  funssres  5627  dffv2  5939  fmptcof  6054  fnprb  6118  fnprOLD  6119  fliftfuns  6199  isorel  6209  caovclg  6450  caovcomg  6453  caovassg  6456  caovcang  6459  caovordig  6463  caovordg  6465  caovdig  6472  caovdirg  6475  peano5  6702  fvmpt2curryd  7000  qliftfuns  7398  nneneq  7700  cfslb  8645  hsmexlem4  8808  axdc3lem2  8830  axdc4lem  8834  adderpq  9333  mulerpq  9334  ltordlem  10077  lble  10494  uz11  11103  xrsupsslem  11497  xrinfmsslem  11498  xrsupss  11499  xrinfmss  11500  fseqsupubi  12055  hashbclem  12466  ccatw2s1p1  12602  swrdswrd  12647  swrdccatin2  12674  cshwcsh2id  12758  wrd2pr2op  12847  wwlktovf  12856  isercolllem1  13449  caucvgb  13464  zsum  13502  fsum  13504  fsumf1o  13507  fsumcvg2  13511  isummulc2  13539  fsum2dlem  13547  fsumcom2  13551  fsumshftm  13558  fsum0diag2  13560  fsum00  13574  fsumrlim  13587  o1fsum  13589  isumshft  13613  dvdsprm  14098  pythagtriplem4  14201  pcmptdvds  14271  proplem  14944  prslem  15417  posi  15436  dlatmjdi  15680  mndlem1  15735  ghmlin  16074  cntzmhm2  16179  dprdss  16875  dprd2d2  16892  srgrz  16976  srglz  16977  lmodlema  17312  islmodd  17313  lsscl  17384  lsslss  17402  lspdisjb  17567  rrgeq0i  17724  assalem  17752  lsslinds  18649  fvmptnn04if  19133  chfacfscmulgsum  19144  chfacfpmmulgsum  19148  ssnei2  19399  t1ficld  19610  t1sep2  19652  uncon  19712  1stcclb  19727  ptbasfi  19833  tx1stc  19902  qtoptop2  19951  r0sep  20000  ustincl  20461  ustdiag  20462  ustinvel  20463  ustexhalf  20464  psmet0  20563  psmettri2  20564  prdsdsf  20621  prdsxmet  20623  cncfi  21149  ovolfiniun  21663  mbfimaopnlem  21813  limciun  22049  dvcn  22075  dvmptfsum  22127  dvfsumle  22173  dvfsumabs  22175  dvfsumlem3  22180  itgsubst  22201  fsumvma  23232  dchrelbasd  23258  dchrisumlem3  23420  axcontlem9  23967  usgranloop0  24072  nbgrassovt  24127  usgra2wlkspthlem2  24312  4cycl4dv  24359  wlklniswwlkn2  24392  numclwwlkovf2ex  24779  grpoass  24897  ghomlin  25058  ghgrplem2  25061  rngodi  25079  rngodir  25080  rngoass  25081  lnolin  25361  elnlfn  26539  strlem4  26865  hstrlem4  26873  atmd  27010  nn0min  27295  slmdlema  27424  esumcvg  27748  measxun2  27837  sibfima  27936  cvmcov  28364  ghomgrpilem1  28516  clim2prod  28615  ntrivcvgfvn0  28626  zprod  28662  fprod  28666  fprodf1o  28671  prodss  28672  fprodser  28674  fprodm1s  28692  fprodp1s  28693  fprodabs  28696  fprodefsum  28697  fprod2dlem  28703  fprodcom2  28707  dfon2lem5  28812  frrlem4  28983  nofulllem5  29059  ifscgr  29287  mbfresfi  29654  nn0prpw  29734  neibastop2lem  29797  totbndss  29892  rngohomadd  29991  rngohommul  29992  crngocom  30017  idladdcl  30035  idllmulcl  30036  idlrmulcl  30037  exlimddvf  30145  elrfirn2  30248  wepwsolem  30607  kelac1  30629  islssfg2  30637  lnmlssfg  30646  2elfz3nn0  31815  2elfz2melfz  31817  bnj110  33004  bnj594  33058  bnj1491  33201  oposlem  33988  cvlexch1  34134  hlsuprexch  34186  lautle  34889
  Copyright terms: Public domain W3C validator