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  3027  vtocl3gf  3028  vtoclegft  3039  sbcthdv  3197  swopolem  4645  funssres  5453  dffv2  5759  fmptcof  5872  fnprb  5931  fnprOLD  5932  fliftfuns  6002  isorel  6012  caovclg  6250  caovcomg  6253  caovassg  6256  caovcang  6259  caovordig  6263  caovordg  6265  caovdig  6272  caovdirg  6275  peano5  6494  qliftfuns  7179  nneneq  7486  cfslb  8427  hsmexlem4  8590  axdc3lem2  8612  axdc4lem  8616  adderpq  9117  mulerpq  9118  ltordlem  9857  lble  10274  uz11  10875  xrsupsslem  11261  xrinfmsslem  11262  xrsupss  11263  xrinfmss  11264  fseqsupubi  11792  hashbclem  12197  swrdswrd  12346  swrdccatin2  12370  wrd2pr2op  12539  isercolllem1  13134  caucvgb  13149  zsum  13187  fsum  13189  fsumf1o  13192  fsumcvg2  13196  isummulc2  13221  fsum2dlem  13229  fsumcom2  13233  fsumshftm  13240  fsum0diag2  13242  fsum00  13253  fsumrlim  13266  o1fsum  13268  isumshft  13294  dvdsprm  13777  pythagtriplem4  13878  pcmptdvds  13948  proplem  14620  prslem  15093  posi  15112  dlatmjdi  15356  mndlem1  15411  ghmlin  15743  cntzmhm2  15848  dprdss  16514  dprd2d2  16531  srgrz  16615  srglz  16616  lmodlema  16931  islmodd  16932  lsscl  17001  lsslss  17019  lspdisjb  17184  rrgeq0i  17337  assalem  17365  lsslinds  18235  ssnei2  18695  t1ficld  18906  t1sep2  18948  uncon  19008  1stcclb  19023  ptbasfi  19129  tx1stc  19198  qtoptop2  19247  r0sep  19296  ustincl  19757  ustdiag  19758  ustinvel  19759  ustexhalf  19760  psmet0  19859  psmettri2  19860  prdsdsf  19917  prdsxmet  19919  cncfi  20445  ovolfiniun  20959  mbfimaopnlem  21108  limciun  21344  dvcn  21370  dvmptfsum  21422  dvfsumle  21468  dvfsumabs  21470  dvfsumlem3  21475  itgsubst  21496  fsumvma  22527  dchrelbasd  22553  dchrisumlem3  22715  axcontlem9  23169  usgranloop0  23250  nbgrassovt  23297  4cycl4dv  23504  grpoass  23641  ghomlin  23802  ghgrplem2  23805  rngodi  23823  rngodir  23824  rngoass  23825  lnolin  24105  elnlfn  25283  strlem4  25609  hstrlem4  25617  atmd  25754  nn0min  26041  slmdlema  26170  esumcvg  26487  measxun2  26576  sibfima  26676  cvmcov  27104  ghomgrpilem1  27255  clim2prod  27354  ntrivcvgfvn0  27365  zprod  27401  fprod  27405  fprodf1o  27410  prodss  27411  fprodser  27413  fprodm1s  27431  fprodp1s  27432  fprodabs  27435  fprodefsum  27436  fprod2dlem  27442  fprodcom2  27446  dfon2lem5  27551  frrlem4  27722  nofulllem5  27798  ifscgr  28026  mbfresfi  28391  nn0prpw  28471  neibastop2lem  28534  totbndss  28629  rngohomadd  28728  rngohommul  28729  crngocom  28754  idladdcl  28772  idllmulcl  28773  idlrmulcl  28774  exlimddvf  28882  elrfirn2  28985  wepwsolem  29347  kelac1  29369  islssfg2  29377  lnmlssfg  29386  2elfz3nn0  30152  2elfz2melfz  30155  wwlktovf  30204  ccatw2s1p1  30222  usgra2wlkspthlem2  30250  wlklniswwlkn2  30287  erclwwlktr0  30432  numclwwlkovf2ex  30632  bnj110  31738  bnj594  31792  bnj1491  31935  oposlem  32667  cvlexch1  32813  hlsuprexch  32865  lautle  33568
  Copyright terms: Public domain W3C validator