MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan9 Structured version   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  |-  ( 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  471  vtocl2gf  3155  vtocl3gf  3156  vtoclegft  3167  sbcthdv  3329  swopolem  4799  funssres  5618  dffv2  5931  fmptcof  6050  fnprb  6114  fnprOLD  6115  fliftfuns  6197  isorel  6207  oveqrspc2v  6304  caovclg  6452  caovcomg  6455  caovassg  6458  caovcang  6461  caovordig  6465  caovordg  6467  caovdig  6474  caovdirg  6477  peano5  6708  fvmpt2curryd  7002  qliftfuns  7400  nneneq  7702  cfslb  8649  hsmexlem4  8812  axdc3lem2  8834  axdc4lem  8838  adderpq  9337  mulerpq  9338  ltordlem  10085  lble  10502  uz11  11114  xrsupsslem  11509  xrinfmsslem  11510  xrsupss  11511  xrinfmss  11512  fseqsupubi  12070  hashbclem  12483  ccatw2s1p1  12622  swrdswrd  12667  swrdccatin2  12694  cshwcsh2id  12778  wrd2pr2op  12867  wwlktovf  12876  isercolllem1  13469  caucvgb  13484  zsum  13522  fsum  13524  fsumf1o  13527  fsumcvg2  13531  isummulc2  13559  fsum2dlem  13567  fsumcom2  13571  fsumshftm  13578  fsum0diag2  13580  fsum00  13594  fsumrlim  13607  o1fsum  13609  isumshft  13633  clim2prod  13679  ntrivcvgfvn0  13690  zprod  13726  fprod  13730  fprodf1o  13735  prodss  13736  fprodser  13738  fprodm1s  13756  fprodp1s  13757  fprodabs  13760  fprod2dlem  13766  fprodcom2  13770  fprodefsum  13812  dvdsprm  14222  pythagtriplem4  14325  pcmptdvds  14395  prslem  15539  posi  15558  dlatmjdi  15803  ghmlin  16251  cntzmhm2  16356  dprdss  17055  dprd2d2  17072  srgrz  17156  srglz  17157  lmodlema  17496  islmodd  17497  lsscl  17568  lsslss  17586  lspdisjb  17751  rrgeq0i  17916  assalem  17944  lsslinds  18844  fvmptnn04if  19328  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  ssnei2  19595  t1ficld  19806  t1sep2  19848  uncon  19908  1stcclb  19923  ptbasfi  20060  tx1stc  20129  qtoptop2  20178  r0sep  20227  ustincl  20688  ustdiag  20689  ustinvel  20690  ustexhalf  20691  psmet0  20790  psmettri2  20791  prdsdsf  20848  prdsxmet  20850  cncfi  21376  ovolfiniun  21890  mbfimaopnlem  22040  limciun  22276  dvcn  22302  dvmptfsum  22354  dvfsumle  22400  dvfsumabs  22402  dvfsumlem3  22407  itgsubst  22428  fsumvma  23466  dchrelbasd  23492  dchrisumlem3  23654  axcontlem9  24253  usgranloop0  24358  nbgrassovt  24413  usgra2wlkspthlem2  24598  4cycl4dv  24645  numclwwlkovf2ex  25064  grpoass  25183  ghomlinOLD  25344  ghgrplem2OLD  25347  rngodi  25365  rngodir  25366  rngoass  25367  lnolin  25647  elnlfn  26825  strlem4  27151  hstrlem4  27159  atmd  27296  nn0min  27589  omndadd  27674  slmdlema  27724  esumcvg  28070  measxun2  28159  sibfima  28258  cvmcov  28686  mrsubcn  28857  ghomgrpilem1  29003  dfon2lem5  29195  frrlem4  29366  nofulllem5  29442  ifscgr  29670  mbfresfi  30037  nn0prpw  30117  neibastop2lem  30154  totbndss  30249  rngohomadd  30348  rngohommul  30349  crngocom  30374  idladdcl  30392  idllmulcl  30393  idlrmulcl  30394  exlimddvf  30502  elrfirn2  30604  wepwsolem  30963  kelac1  30985  islssfg2  30993  lnmlssfg  31002  2elfz3nn0  32286  2elfz2melfz  32288  bnj110  33784  bnj594  33838  bnj1491  33981  oposlem  34782  cvlexch1  34928  hlsuprexch  34980  lautle  35683
  Copyright terms: Public domain W3C validator