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

Theorem mpan9 455
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 28 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 419 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylan  457  vtocl2gf  2845  vtocl3gf  2846  vtoclegft  2855  sbcthdv  3006  swopolem  4323  peano5  4679  funssres  5294  dffv2  5592  fmptcof  5692  fliftfuns  5813  isorel  5823  caovclg  6012  caovcomg  6015  caovassg  6018  caovcang  6021  caovordig  6025  caovordg  6027  caovdig  6034  caovdirg  6037  qliftfuns  6745  nneneq  7044  cfslb  7892  hsmexlem4  8055  axdc3lem2  8077  axdc4lem  8081  adderpq  8580  mulerpq  8581  ltordlem  9298  lble  9706  uz11  10250  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  fseqsupubi  11040  hashbclem  11390  isercolllem1  12138  caucvgb  12152  zsum  12191  fsum  12193  fsumf1o  12196  fsumcvg2  12200  isummulc2  12225  fsum2dlem  12233  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsum00  12256  fsumrlim  12269  o1fsum  12271  isumshft  12298  dvdsprm  12778  pythagtriplem4  12872  pcmptdvds  12942  proplem  13592  prslem  14065  posi  14084  clatlem  14216  dlatmjdi  14297  laspwcl  14343  lanfwcl  14344  mndlem1  14371  ghmlin  14688  cntzmhm2  14815  dprdss  15264  dprd2d2  15279  lmodlema  15632  islmodd  15633  lsscl  15700  lsslss  15718  lspdisjb  15879  rrgeq0i  16030  assalem  16057  ssnei2  16853  t1ficld  17055  t1sep2  17097  uncon  17155  1stcclb  17170  ptbasfi  17276  tx1stc  17344  qtoptop2  17390  r0sep  17439  prdsdsf  17931  prdsxmet  17933  cncfi  18398  ovolfiniun  18860  mbfimaopnlem  19010  limciun  19244  dvcn  19270  dvmptfsum  19322  dvfsumle  19368  dvfsumabs  19370  dvfsumlem3  19375  itgsubst  19396  fsumvma  20452  dchrelbasd  20478  dchrisumlem3  20640  grpoass  20870  ghomlin  21031  ghgrplem2  21034  rngodi  21052  rngodir  21053  rngoass  21054  lnolin  21332  elnlfn  22508  strlem4  22834  hstrlem4  22842  atmd  22979  esumcvg  23454  measxun2  23538  cvmcov  23794  ghomgrpilem1  23992  dfon2lem5  24143  frrlem4  24284  nofulllem5  24360  axcontlem9  24600  ifscgr  24667  eqfnung2  25118  repfuntw  25160  smgrpass2  25341  reacomsmgrp2  25344  resgcom  25351  fprodadd  25352  mndoass2  25360  fprodneg  25378  fprodsub  25379  vecax5b  25459  osneisi  25531  imonclem  25813  partarelt1  25896  fnctartar  25907  fnctartar2  25908  lemindclsbu  25995  nn0prpw  26239  neibastop2lem  26309  totbndss  26501  rngohomadd  26600  rngohommul  26601  crngocom  26626  idladdcl  26644  idllmulcl  26645  idlrmulcl  26646  elrfirn2  26771  wepwsolem  27138  kelac1  27161  islssfg2  27169  lnmlssfg  27178  lsslinds  27301  nbgrassovt  28150  bnj110  28890  bnj594  28944  oposlem  29373  cvlexch1  29518  hlsuprexch  29570  lautle  30273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator