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

Theorem mpan9 467
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 30 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 428 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  sylan  469  vtocl2gf  3118  vtocl3gf  3119  vtoclegft  3130  sbcthdv  3292  swopolem  4752  funssres  5608  dffv2  5921  fmptcof  6043  fnprb  6109  fliftfuns  6194  isorel  6204  oveqrspc2v  6300  caovclg  6447  caovcomg  6450  caovassg  6453  caovcang  6456  caovordig  6460  caovordg  6462  caovdig  6469  caovdirg  6472  peano5  6706  fvmpt2curryd  7002  qliftfuns  7434  nneneq  7737  cfslb  8677  hsmexlem4  8840  axdc3lem2  8862  axdc4lem  8866  adderpq  9363  mulerpq  9364  ltordlem  10117  lble  10534  uz11  11148  xrsupsslem  11550  xrinfmsslem  11551  xrsupss  11552  xrinfmss  11553  fseqsupubi  12127  hashbclem  12548  swrdswrd  12739  swrdccatin2  12766  cshwcsh2id  12850  wrd2pr2op  12939  wwlktovf  12948  isercolllem1  13634  caucvgb  13649  zsum  13687  fsum  13689  fsumf1o  13692  fsumcvg2  13696  isummulc2  13726  fsum2dlem  13734  fsumcom2  13738  fsumshftm  13745  fsum0diag2  13747  fsum00  13761  fsumrlim  13774  o1fsum  13776  isumshft  13800  clim2prod  13847  ntrivcvgfvn0  13858  zprod  13894  fprod  13898  fprodf1o  13903  prodss  13904  fprodser  13906  fprodm1s  13924  fprodp1s  13925  fprodabs  13928  fprod2dlem  13934  fprodcom2  13938  fprodefsum  14037  dvdsprm  14447  pythagtriplem4  14550  pcmptdvds  14620  prslem  15882  posi  15901  dlatmjdi  16146  ghmlin  16594  cntzmhm2  16699  dprdss  17394  dprd2d2  17411  srgrz  17495  srglz  17496  lmodlema  17835  islmodd  17836  lsscl  17907  lsslss  17925  lspdisjb  18090  rrgeq0i  18255  assalem  18283  lsslinds  19156  fvmptnn04if  19640  chfacfscmulgsum  19651  chfacfpmmulgsum  19655  ssnei2  19908  t1ficld  20119  t1sep2  20161  uncon  20220  1stcclb  20235  ptbasfi  20372  tx1stc  20441  qtoptop2  20490  r0sep  20539  ustincl  21000  ustdiag  21001  ustinvel  21002  ustexhalf  21003  psmet0  21102  psmettri2  21103  prdsdsf  21160  prdsxmet  21162  cncfi  21688  ovolfiniun  22202  mbfimaopnlem  22352  limciun  22588  dvcn  22614  dvmptfsum  22666  dvfsumle  22712  dvfsumabs  22714  dvfsumlem3  22719  itgsubst  22740  fsumvma  23867  dchrelbasd  23893  dchrisumlem3  24055  axcontlem9  24679  usgranloop0  24784  nbgrassovt  24839  usgra2wlkspthlem2  25024  4cycl4dv  25071  numclwwlkovf2ex  25490  grpoass  25605  ghomlinOLD  25766  ghgrplem2OLD  25769  rngodi  25787  rngodir  25788  rngoass  25789  lnolin  26069  elnlfn  27246  strlem4  27572  hstrlem4  27580  atmd  27717  nn0min  28049  omndadd  28134  slmdlema  28184  esumcvg  28519  measxun2  28644  sibfima  28772  bnj110  29230  bnj594  29284  bnj1491  29427  cvmcov  29547  mrsubcn  29718  ghomgrpilem1  29864  dfon2lem5  29993  frrlem4  30077  nofulllem5  30153  ifscgr  30369  nn0prpw  30538  neibastop2lem  30575  mbfresfi  31413  totbndss  31535  rngohomadd  31634  rngohommul  31635  crngocom  31660  idladdcl  31678  idllmulcl  31679  idlrmulcl  31680  exlimddvf  31788  oposlem  32180  cvlexch1  32326  hlsuprexch  32378  lautle  33081  elrfirn2  34970  wepwsolem  35329  kelac1  35351  islssfg2  35359  lnmlssfg  35368  mod2eq1n2dvds  37657  icceuelpartlem  37683  wtgoldbnnsum4prm  37831  bgoldbnnsum3prm  37833  bgoldbtbnd  37838  2elfz3nn0  37945  2elfz2melfz  37947
  Copyright terms: Public domain W3C validator