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  3138  vtocl3gf  3139  vtoclegft  3150  sbcthdv  3310  swopolem  4761  funssres  5569  dffv2  5876  fmptcof  5989  fnprb  6048  fnprOLD  6049  fliftfuns  6119  isorel  6129  caovclg  6368  caovcomg  6371  caovassg  6374  caovcang  6377  caovordig  6381  caovordg  6383  caovdig  6390  caovdirg  6393  peano5  6612  fvmpt2curryd  6903  qliftfuns  7300  nneneq  7607  cfslb  8549  hsmexlem4  8712  axdc3lem2  8734  axdc4lem  8738  adderpq  9239  mulerpq  9240  ltordlem  9979  lble  10396  uz11  10997  xrsupsslem  11383  xrinfmsslem  11384  xrsupss  11385  xrinfmss  11386  fseqsupubi  11920  hashbclem  12326  swrdswrd  12475  swrdccatin2  12499  wrd2pr2op  12668  isercolllem1  13263  caucvgb  13278  zsum  13316  fsum  13318  fsumf1o  13321  fsumcvg2  13325  isummulc2  13350  fsum2dlem  13358  fsumcom2  13362  fsumshftm  13369  fsum0diag2  13371  fsum00  13382  fsumrlim  13395  o1fsum  13397  isumshft  13423  dvdsprm  13906  pythagtriplem4  14007  pcmptdvds  14077  proplem  14750  prslem  15223  posi  15242  dlatmjdi  15486  mndlem1  15541  ghmlin  15874  cntzmhm2  15979  dprdss  16651  dprd2d2  16668  srgrz  16752  srglz  16753  lmodlema  17079  islmodd  17080  lsscl  17150  lsslss  17168  lspdisjb  17333  rrgeq0i  17486  assalem  17514  lsslinds  18388  ssnei2  18855  t1ficld  19066  t1sep2  19108  uncon  19168  1stcclb  19183  ptbasfi  19289  tx1stc  19358  qtoptop2  19407  r0sep  19456  ustincl  19917  ustdiag  19918  ustinvel  19919  ustexhalf  19920  psmet0  20019  psmettri2  20020  prdsdsf  20077  prdsxmet  20079  cncfi  20605  ovolfiniun  21119  mbfimaopnlem  21269  limciun  21505  dvcn  21531  dvmptfsum  21583  dvfsumle  21629  dvfsumabs  21631  dvfsumlem3  21636  itgsubst  21657  fsumvma  22688  dchrelbasd  22714  dchrisumlem3  22876  axcontlem9  23390  usgranloop0  23471  nbgrassovt  23518  4cycl4dv  23725  grpoass  23862  ghomlin  24023  ghgrplem2  24026  rngodi  24044  rngodir  24045  rngoass  24046  lnolin  24326  elnlfn  25504  strlem4  25830  hstrlem4  25838  atmd  25975  nn0min  26255  slmdlema  26384  esumcvg  26700  measxun2  26789  sibfima  26888  cvmcov  27316  ghomgrpilem1  27468  clim2prod  27567  ntrivcvgfvn0  27578  zprod  27614  fprod  27618  fprodf1o  27623  prodss  27624  fprodser  27626  fprodm1s  27644  fprodp1s  27645  fprodabs  27648  fprodefsum  27649  fprod2dlem  27655  fprodcom2  27659  dfon2lem5  27764  frrlem4  27935  nofulllem5  28011  ifscgr  28239  mbfresfi  28606  nn0prpw  28686  neibastop2lem  28749  totbndss  28844  rngohomadd  28943  rngohommul  28944  crngocom  28969  idladdcl  28987  idllmulcl  28988  idlrmulcl  28989  exlimddvf  29097  elrfirn2  29200  wepwsolem  29562  kelac1  29584  islssfg2  29592  lnmlssfg  29601  2elfz3nn0  30367  2elfz2melfz  30370  wwlktovf  30419  ccatw2s1p1  30437  usgra2wlkspthlem2  30465  wlklniswwlkn2  30502  erclwwlktr0  30647  numclwwlkovf2ex  30847  fvmptnn04if  31355  chfacfscmulgsum  31366  chfacfpmmulgsum  31370  bnj110  32203  bnj594  32257  bnj1491  32400  oposlem  33185  cvlexch1  33331  hlsuprexch  33383  lautle  34086
  Copyright terms: Public domain W3C validator