MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan9 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
mpan9.2
Assertion
Ref Expression
mpan9

Proof of Theorem mpan9
StepHypRef Expression
1 mpan9.1 . . 3
2 mpan9.2 . . 3
31, 2syl5 32 . 2
43impcom 430 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sylan  471  vtocl2gf  3169  vtocl3gf  3170  vtoclegft  3181  sbcthdv  3343  swopolem  4814  funssres  5633  dffv2  5946  fmptcof  6065  fnprb  6129  fnprOLD  6130  fliftfuns  6212  isorel  6222  oveqrspc2v  6319  caovclg  6467  caovcomg  6470  caovassg  6473  caovcang  6476  caovordig  6480  caovordg  6482  caovdig  6489  caovdirg  6492  peano5  6723  fvmpt2curryd  7019  qliftfuns  7417  nneneq  7720  cfslb  8667  hsmexlem4  8830  axdc3lem2  8852  axdc4lem  8856  adderpq  9355  mulerpq  9356  ltordlem  10103  lble  10520  uz11  11132  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  fseqsupubi  12088  hashbclem  12501  ccatw2s1p1  12640  swrdswrd  12685  swrdccatin2  12712  cshwcsh2id  12796  wrd2pr2op  12885  wwlktovf  12894  isercolllem1  13487  caucvgb  13502  zsum  13540  fsum  13542  fsumf1o  13545  fsumcvg2  13549  isummulc2  13577  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  fsum00  13612  fsumrlim  13625  o1fsum  13627  isumshft  13651  clim2prod  13697  ntrivcvgfvn0  13708  zprod  13744  fprod  13748  fprodf1o  13753  prodss  13754  fprodser  13756  fprodm1s  13774  fprodp1s  13775  fprodabs  13778  fprod2dlem  13784  fprodcom2  13788  fprodefsum  13830  dvdsprm  14240  pythagtriplem4  14343  pcmptdvds  14413  prslem  15560  posi  15579  dlatmjdi  15824  ghmlin  16272  cntzmhm2  16377  dprdss  17076  dprd2d2  17093  srgrz  17177  srglz  17178  lmodlema  17517  islmodd  17518  lsscl  17589  lsslss  17607  lspdisjb  17772  rrgeq0i  17937  assalem  17965  lsslinds  18866  fvmptnn04if  19350  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  ssnei2  19617  t1ficld  19828  t1sep2  19870  uncon  19930  1stcclb  19945  ptbasfi  20082  tx1stc  20151  qtoptop2  20200  r0sep  20249  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  psmet0  20812  psmettri2  20813  prdsdsf  20870  prdsxmet  20872  cncfi  21398  ovolfiniun  21912  mbfimaopnlem  22062  limciun  22298  dvcn  22324  dvmptfsum  22376  dvfsumle  22422  dvfsumabs  22424  dvfsumlem3  22429  itgsubst  22450  fsumvma  23488  dchrelbasd  23514  dchrisumlem3  23676  axcontlem9  24275  usgranloop0  24380  nbgrassovt  24435  usgra2wlkspthlem2  24620  4cycl4dv  24667  numclwwlkovf2ex  25086  grpoass  25205  ghomlinOLD  25366  ghgrplem2OLD  25369  rngodi  25387  rngodir  25388  rngoass  25389  lnolin  25669  elnlfn  26847  strlem4  27173  hstrlem4  27181  atmd  27318  nn0min  27611  omndadd  27696  slmdlema  27746  esumcvg  28092  measxun2  28181  sibfima  28280  cvmcov  28708  mrsubcn  28879  ghomgrpilem1  29025  dfon2lem5  29219  frrlem4  29390  nofulllem5  29466  ifscgr  29694  mbfresfi  30061  nn0prpw  30141  neibastop2lem  30178  totbndss  30273  rngohomadd  30372  rngohommul  30373  crngocom  30398  idladdcl  30416  idllmulcl  30417  idlrmulcl  30418  exlimddvf  30526  elrfirn2  30628  wepwsolem  30987  kelac1  31009  islssfg2  31017  lnmlssfg  31026  2elfz3nn0  32332  2elfz2melfz  32334  bnj110  33916  bnj594  33970  bnj1491  34113  oposlem  34907  cvlexch1  35053  hlsuprexch  35105  lautle  35808
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
  Copyright terms: Public domain W3C validator