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  2858  vtocl3gf  2859  vtoclegft  2868  sbcthdv  3019  swopolem  4339  peano5  4695  funssres  5310  dffv2  5608  fmptcof  5708  fliftfuns  5829  isorel  5839  caovclg  6028  caovcomg  6031  caovassg  6034  caovcang  6037  caovordig  6041  caovordg  6043  caovdig  6050  caovdirg  6053  qliftfuns  6761  nneneq  7060  cfslb  7908  hsmexlem4  8071  axdc3lem2  8093  axdc4lem  8097  adderpq  8596  mulerpq  8597  ltordlem  9314  lble  9722  uz11  10266  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  fseqsupubi  11056  hashbclem  11406  isercolllem1  12154  caucvgb  12168  zsum  12207  fsum  12209  fsumf1o  12212  fsumcvg2  12216  isummulc2  12241  fsum2dlem  12249  fsumcom2  12253  fsumshftm  12259  fsum0diag2  12261  fsum00  12272  fsumrlim  12285  o1fsum  12287  isumshft  12314  dvdsprm  12794  pythagtriplem4  12888  pcmptdvds  12958  proplem  13608  prslem  14081  posi  14100  clatlem  14232  dlatmjdi  14313  laspwcl  14359  lanfwcl  14360  mndlem1  14387  ghmlin  14704  cntzmhm2  14831  dprdss  15280  dprd2d2  15295  lmodlema  15648  islmodd  15649  lsscl  15716  lsslss  15734  lspdisjb  15895  rrgeq0i  16046  assalem  16073  ssnei2  16869  t1ficld  17071  t1sep2  17113  uncon  17171  1stcclb  17186  ptbasfi  17292  tx1stc  17360  qtoptop2  17406  r0sep  17455  prdsdsf  17947  prdsxmet  17949  cncfi  18414  ovolfiniun  18876  mbfimaopnlem  19026  limciun  19260  dvcn  19286  dvmptfsum  19338  dvfsumle  19384  dvfsumabs  19386  dvfsumlem3  19391  itgsubst  19412  fsumvma  20468  dchrelbasd  20494  dchrisumlem3  20656  grpoass  20886  ghomlin  21047  ghgrplem2  21050  rngodi  21068  rngodir  21069  rngoass  21070  lnolin  21348  elnlfn  22524  strlem4  22850  hstrlem4  22858  atmd  22995  esumcvg  23469  measxun2  23553  cvmcov  23809  ghomgrpilem1  24007  zprod  24160  fprod  24164  fprodf1o  24172  dfon2lem5  24214  frrlem4  24355  nofulllem5  24431  axcontlem9  24672  ifscgr  24739  eqfnung2  25221  repfuntw  25263  smgrpass2  25444  reacomsmgrp2  25447  resgcom  25454  fprodadd  25455  mndoass2  25463  fprodneg  25481  fprodsub  25482  vecax5b  25562  osneisi  25634  imonclem  25916  partarelt1  25999  fnctartar  26010  fnctartar2  26011  lemindclsbu  26098  nn0prpw  26342  neibastop2lem  26412  totbndss  26604  rngohomadd  26703  rngohommul  26704  crngocom  26729  idladdcl  26747  idllmulcl  26748  idlrmulcl  26749  elrfirn2  26874  wepwsolem  27241  kelac1  27264  islssfg2  27272  lnmlssfg  27281  lsslinds  27404  nbgrassovt  28284  4cycl4dv  28413  bnj110  29206  bnj594  29260  oposlem  29995  cvlexch1  30140  hlsuprexch  30192  lautle  30895
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