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

Theorem mpan9 456
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 30 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 420 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylan  458  vtocl2gf  2973  vtocl3gf  2974  vtoclegft  2983  sbcthdv  3136  swopolem  4472  peano5  4827  funssres  5452  dffv2  5755  fmptcof  5861  fnpr  5909  fnprOLD  5910  fliftfuns  5995  isorel  6005  caovclg  6198  caovcomg  6201  caovassg  6204  caovcang  6207  caovordig  6211  caovordg  6213  caovdig  6220  caovdirg  6223  qliftfuns  6950  nneneq  7249  cfslb  8102  hsmexlem4  8265  axdc3lem2  8287  axdc4lem  8291  adderpq  8789  mulerpq  8790  ltordlem  9508  lble  9916  uz11  10464  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  fseqsupubi  11272  hashbclem  11656  isercolllem1  12413  caucvgb  12428  zsum  12467  fsum  12469  fsumf1o  12472  fsumcvg2  12476  isummulc2  12501  fsum2dlem  12509  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsum00  12532  fsumrlim  12545  o1fsum  12547  isumshft  12574  dvdsprm  13054  pythagtriplem4  13148  pcmptdvds  13218  proplem  13870  prslem  14343  posi  14362  clatlem  14494  dlatmjdi  14575  laspwcl  14621  lanfwcl  14622  mndlem1  14649  ghmlin  14966  cntzmhm2  15093  dprdss  15542  dprd2d2  15557  lmodlema  15910  islmodd  15911  lsscl  15974  lsslss  15992  lspdisjb  16153  rrgeq0i  16304  assalem  16331  ssnei2  17135  t1ficld  17345  t1sep2  17387  uncon  17445  1stcclb  17460  ptbasfi  17566  tx1stc  17635  qtoptop2  17684  r0sep  17733  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  psmet0  18292  psmettri2  18293  prdsdsf  18350  prdsxmet  18352  cncfi  18877  ovolfiniun  19350  mbfimaopnlem  19500  limciun  19734  dvcn  19760  dvmptfsum  19812  dvfsumle  19858  dvfsumabs  19860  dvfsumlem3  19865  itgsubst  19886  fsumvma  20950  dchrelbasd  20976  dchrisumlem3  21138  usgranloop0  21353  nbgrassovt  21400  4cycl4dv  21607  grpoass  21744  ghomlin  21905  ghgrplem2  21908  rngodi  21926  rngodir  21927  rngoass  21928  lnolin  22208  elnlfn  23384  strlem4  23710  hstrlem4  23718  atmd  23855  esumcvg  24429  measxun2  24517  sibfima  24606  cvmcov  24903  ghomgrpilem1  25049  clim2prod  25169  ntrivcvgfvn0  25180  zprod  25216  fprod  25220  fprodf1o  25225  prodss  25226  fprodser  25228  fprodm1s  25246  fprodp1s  25247  fprodabs  25250  fprodefsum  25251  fprod2dlem  25257  fprodcom2  25261  dfon2lem5  25357  frrlem4  25498  nofulllem5  25574  axcontlem9  25815  ifscgr  25882  mbfresfi  26152  nn0prpw  26216  neibastop2lem  26279  totbndss  26376  rngohomadd  26475  rngohommul  26476  crngocom  26501  idladdcl  26519  idllmulcl  26520  idlrmulcl  26521  elrfirn2  26640  wepwsolem  27006  kelac1  27029  islssfg2  27037  lnmlssfg  27046  lsslinds  27169  2elfz3nn0  27984  swrdswrd  28011  swrdccatin12b  28027  usgra2wlkspthlem2  28037  bnj110  28935  bnj594  28989  bnj1491  29132  oposlem  29666  cvlexch1  29811  hlsuprexch  29863  lautle  30566
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 178  df-an 361
  Copyright terms: Public domain W3C validator