MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan9 Structured version   Visualization 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 33 . 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  3111  vtocl3gf  3112  vtoclegft  3123  sbcthdv  3285  swopolem  4767  funssres  5625  dffv2  5943  fmptcof  6062  fnprb  6128  fliftfuns  6212  isorel  6222  oveqrspc2v  6318  caovclg  6466  caovcomg  6469  caovassg  6472  caovcang  6475  caovordig  6479  caovordg  6481  caovdig  6488  caovdirg  6491  peano5  6721  fvmpt2curryd  7023  qliftfuns  7455  nneneq  7760  cfslb  8701  hsmexlem4  8864  axdc3lem2  8886  axdc4lem  8890  adderpq  9386  mulerpq  9387  ltordlem  10146  lble  10565  uz11  11188  xrsupsslem  11599  xrinfmsslem  11600  xrsupss  11601  xrinfmss  11602  fseqsupubi  12198  hashbclem  12622  swrdswrd  12823  swrdccatin2  12850  cshwcsh2id  12934  wrd2pr2op  13034  wwlktovf  13043  isercolllem1  13740  caucvgb  13758  zsum  13796  fsum  13798  fsumf1o  13801  fsumcvg2  13805  isummulc2  13835  fsum2dlem  13843  fsumcom2  13847  fsumshftm  13854  fsum0diag2  13856  fsum00  13870  fsumrlim  13883  o1fsum  13885  isumshft  13909  clim2prod  13956  ntrivcvgfvn0  13967  zprod  14003  fprod  14007  fprodf1o  14012  prodss  14013  fprodser  14015  fprodm1s  14036  fprodp1s  14037  fprodabs  14040  fprod2dlem  14046  fprodcom2  14050  fprodefsum  14161  lcmfun  14630  dvdsprm  14659  pythagtriplem4  14781  pcmptdvds  14851  prslem  16188  posi  16207  dlatmjdi  16452  ghmlin  16900  cntzmhm2  17005  dprdss  17674  dprd2d2  17689  srgrz  17771  srglz  17772  lmodlema  18108  islmodd  18109  lsscl  18178  lsslss  18196  lspdisjb  18361  rrgeq0i  18525  assalem  18552  lsslinds  19401  fvmptnn04if  19885  chfacfscmulgsum  19896  chfacfpmmulgsum  19900  ssnei2  20144  t1ficld  20355  t1sep2  20397  uncon  20456  1stcclb  20471  ptbasfi  20608  tx1stc  20677  qtoptop2  20726  r0sep  20775  ustincl  21234  ustdiag  21235  ustinvel  21236  ustexhalf  21237  psmet0  21336  psmettri2  21337  prdsdsf  21394  prdsxmet  21396  cncfi  21938  ovolfiniun  22466  mbfimaopnlem  22623  limciun  22861  dvcn  22887  dvmptfsum  22939  dvfsumle  22985  dvfsumabs  22987  dvfsumlem3  22992  itgsubst  23013  fsumvma  24153  dchrelbasd  24179  dchrisumlem3  24341  axcontlem9  25014  usgranloop0  25119  nbgrassovt  25175  usgra2wlkspthlem2  25360  4cycl4dv  25407  numclwwlkovf2ex  25826  grpoass  25943  ghomlinOLD  26104  ghgrplem2OLD  26107  rngodi  26125  rngodir  26126  rngoass  26127  lnolin  26407  elnlfn  27593  strlem4  27919  hstrlem4  27927  atmd  28064  nn0min  28396  omndadd  28481  slmdlema  28531  esumcvg  28919  measxun2  29044  sibfima  29183  bnj110  29681  bnj594  29735  bnj1491  29878  cvmcov  29998  mrsubcn  30169  ghomgrpilem1  30315  dfon2lem5  30445  frrlem4  30529  nofulllem5  30607  ifscgr  30823  nn0prpw  30991  neibastop2lem  31028  poimirlem25  31977  poimirlem32  31984  mbfresfi  31999  totbndss  32121  rngohomadd  32220  rngohommul  32221  crngocom  32246  idladdcl  32264  idllmulcl  32265  idlrmulcl  32266  exlimddvf  32373  oposlem  32760  cvlexch1  32906  hlsuprexch  32958  lautle  33661  elrfirn2  35550  wepwsolem  35912  kelac1  35933  islssfg2  35941  lnmlssfg  35950  mod2eq1n2dvds  38735  icceuelpartlem  38759  wtgoldbnnsum4prm  38907  bgoldbnnsum3prm  38909  bgoldbtbnd  38914  2elfz3nn0  39066  2elfz2melfz  39068  usgruspgrb  39278  umgr2v2evtxel  39569
  Copyright terms: Public domain W3C validator