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

Theorem mpan9 466
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  468  vtocl2gf  3021  vtocl3gf  3022  vtoclegft  3033  sbcthdv  3190  swopolem  4637  funssres  5446  dffv2  5752  fmptcof  5864  fnprb  5923  fnprOLD  5924  fliftfuns  5994  isorel  6004  caovclg  6244  caovcomg  6247  caovassg  6250  caovcang  6253  caovordig  6257  caovordg  6259  caovdig  6266  caovdirg  6269  peano5  6488  qliftfuns  7175  nneneq  7482  cfslb  8423  hsmexlem4  8586  axdc3lem2  8608  axdc4lem  8612  adderpq  9112  mulerpq  9113  ltordlem  9852  lble  10269  uz11  10870  xrsupsslem  11256  xrinfmsslem  11257  xrsupss  11258  xrinfmss  11259  fseqsupubi  11783  hashbclem  12188  swrdswrd  12337  swrdccatin2  12361  wrd2pr2op  12530  isercolllem1  13125  caucvgb  13140  zsum  13178  fsum  13180  fsumf1o  13183  fsumcvg2  13187  isummulc2  13212  fsum2dlem  13220  fsumcom2  13224  fsumshftm  13230  fsum0diag2  13232  fsum00  13243  fsumrlim  13256  o1fsum  13258  isumshft  13284  dvdsprm  13767  pythagtriplem4  13868  pcmptdvds  13938  proplem  14610  prslem  15083  posi  15102  dlatmjdi  15346  mndlem1  15401  ghmlin  15731  cntzmhm2  15836  dprdss  16499  dprd2d2  16516  lmodlema  16876  islmodd  16877  lsscl  16945  lsslss  16963  lspdisjb  17128  rrgeq0i  17281  assalem  17309  lsslinds  18101  ssnei2  18561  t1ficld  18772  t1sep2  18814  uncon  18874  1stcclb  18889  ptbasfi  18995  tx1stc  19064  qtoptop2  19113  r0sep  19162  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  psmet0  19725  psmettri2  19726  prdsdsf  19783  prdsxmet  19785  cncfi  20311  ovolfiniun  20825  mbfimaopnlem  20974  limciun  21210  dvcn  21236  dvmptfsum  21288  dvfsumle  21334  dvfsumabs  21336  dvfsumlem3  21341  itgsubst  21362  fsumvma  22436  dchrelbasd  22462  dchrisumlem3  22624  axcontlem9  23040  usgranloop0  23121  nbgrassovt  23168  4cycl4dv  23375  grpoass  23512  ghomlin  23673  ghgrplem2  23676  rngodi  23694  rngodir  23695  rngoass  23696  lnolin  23976  elnlfn  25154  strlem4  25480  hstrlem4  25488  atmd  25625  nn0min  25912  srgrz  26060  slmdlema  26067  esumcvg  26388  measxun2  26477  sibfima  26571  cvmcov  26999  ghomgrpilem1  27150  clim2prod  27249  ntrivcvgfvn0  27260  zprod  27296  fprod  27300  fprodf1o  27305  prodss  27306  fprodser  27308  fprodm1s  27326  fprodp1s  27327  fprodabs  27330  fprodefsum  27331  fprod2dlem  27337  fprodcom2  27341  dfon2lem5  27446  frrlem4  27617  nofulllem5  27693  ifscgr  27921  mbfresfi  28279  nn0prpw  28359  neibastop2lem  28422  totbndss  28517  rngohomadd  28616  rngohommul  28617  crngocom  28642  idladdcl  28660  idllmulcl  28661  idlrmulcl  28662  exlimddvf  28770  elrfirn2  28874  wepwsolem  29236  kelac1  29258  islssfg2  29266  lnmlssfg  29275  2elfz3nn0  30042  2elfz2melfz  30045  wwlktovf  30094  ccatw2s1p1  30112  usgra2wlkspthlem2  30140  wlklniswwlkn2  30177  erclwwlktr0  30322  numclwwlkovf2ex  30522  bnj110  31550  bnj594  31604  bnj1491  31747  oposlem  32397  cvlexch1  32543  hlsuprexch  32595  lautle  33298
  Copyright terms: Public domain W3C validator