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

Theorem mpan9 472
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 34 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 432 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  sylan  474  vtocl2gf  3142  vtocl3gf  3143  vtoclegft  3154  sbcthdv  3316  swopolem  4781  funssres  5639  dffv2  5952  fmptcof  6070  fnprb  6136  fliftfuns  6220  isorel  6230  oveqrspc2v  6326  caovclg  6473  caovcomg  6476  caovassg  6479  caovcang  6482  caovordig  6486  caovordg  6488  caovdig  6495  caovdirg  6498  peano5  6728  fvmpt2curryd  7024  qliftfuns  7456  nneneq  7759  cfslb  8698  hsmexlem4  8861  axdc3lem2  8883  axdc4lem  8887  adderpq  9383  mulerpq  9384  ltordlem  10141  lble  10560  uz11  11183  xrsupsslem  11594  xrinfmsslem  11595  xrsupss  11596  xrinfmss  11597  fseqsupubi  12192  hashbclem  12614  swrdswrd  12812  swrdccatin2  12839  cshwcsh2id  12923  wrd2pr2op  13016  wwlktovf  13025  isercolllem1  13721  caucvgb  13739  zsum  13777  fsum  13779  fsumf1o  13782  fsumcvg2  13786  isummulc2  13816  fsum2dlem  13824  fsumcom2  13828  fsumshftm  13835  fsum0diag2  13837  fsum00  13851  fsumrlim  13864  o1fsum  13866  isumshft  13890  clim2prod  13937  ntrivcvgfvn0  13948  zprod  13984  fprod  13988  fprodf1o  13993  prodss  13994  fprodser  13996  fprodm1s  14017  fprodp1s  14018  fprodabs  14021  fprod2dlem  14027  fprodcom2  14031  fprodefsum  14142  lcmfun  14611  dvdsprm  14640  pythagtriplem4  14762  pcmptdvds  14832  prslem  16169  posi  16188  dlatmjdi  16433  ghmlin  16881  cntzmhm2  16986  dprdss  17655  dprd2d2  17670  srgrz  17752  srglz  17753  lmodlema  18089  islmodd  18090  lsscl  18159  lsslss  18177  lspdisjb  18342  rrgeq0i  18506  assalem  18533  lsslinds  19381  fvmptnn04if  19865  chfacfscmulgsum  19876  chfacfpmmulgsum  19880  ssnei2  20124  t1ficld  20335  t1sep2  20377  uncon  20436  1stcclb  20451  ptbasfi  20588  tx1stc  20657  qtoptop2  20706  r0sep  20755  ustincl  21214  ustdiag  21215  ustinvel  21216  ustexhalf  21217  psmet0  21316  psmettri2  21317  prdsdsf  21374  prdsxmet  21376  cncfi  21918  ovolfiniun  22446  mbfimaopnlem  22603  limciun  22841  dvcn  22867  dvmptfsum  22919  dvfsumle  22965  dvfsumabs  22967  dvfsumlem3  22972  itgsubst  22993  fsumvma  24133  dchrelbasd  24159  dchrisumlem3  24321  axcontlem9  24994  usgranloop0  25099  nbgrassovt  25155  usgra2wlkspthlem2  25340  4cycl4dv  25387  numclwwlkovf2ex  25806  grpoass  25923  ghomlinOLD  26084  ghgrplem2OLD  26087  rngodi  26105  rngodir  26106  rngoass  26107  lnolin  26387  elnlfn  27573  strlem4  27899  hstrlem4  27907  atmd  28044  nn0min  28385  omndadd  28470  slmdlema  28520  esumcvg  28909  measxun2  29034  sibfima  29173  bnj110  29671  bnj594  29725  bnj1491  29868  cvmcov  29988  mrsubcn  30159  ghomgrpilem1  30305  dfon2lem5  30434  frrlem4  30518  nofulllem5  30594  ifscgr  30810  nn0prpw  30978  neibastop2lem  31015  poimirlem25  31923  poimirlem32  31930  mbfresfi  31945  totbndss  32067  rngohomadd  32166  rngohommul  32167  crngocom  32192  idladdcl  32210  idllmulcl  32211  idlrmulcl  32212  exlimddvf  32319  oposlem  32711  cvlexch1  32857  hlsuprexch  32909  lautle  33612  elrfirn2  35501  wepwsolem  35864  kelac1  35885  islssfg2  35893  lnmlssfg  35902  mod2eq1n2dvds  38481  icceuelpartlem  38505  wtgoldbnnsum4prm  38653  bgoldbnnsum3prm  38655  bgoldbtbnd  38660  2elfz3nn0  38789  2elfz2melfz  38791  usgruspgrb  38937
  Copyright terms: Public domain W3C validator