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  2956  vtocl3gf  2957  vtoclegft  2966  sbcthdv  3119  swopolem  4453  peano5  4808  funssres  5433  dffv2  5735  fmptcof  5841  fnpr  5889  fnprOLD  5890  fliftfuns  5975  isorel  5985  caovclg  6178  caovcomg  6181  caovassg  6184  caovcang  6187  caovordig  6191  caovordg  6193  caovdig  6200  caovdirg  6203  qliftfuns  6927  nneneq  7226  cfslb  8079  hsmexlem4  8242  axdc3lem2  8264  axdc4lem  8268  adderpq  8766  mulerpq  8767  ltordlem  9484  lble  9892  uz11  10440  xrsupsslem  10817  xrinfmsslem  10818  xrsupss  10819  xrinfmss  10820  fseqsupubi  11244  hashbclem  11628  isercolllem1  12385  caucvgb  12400  zsum  12439  fsum  12441  fsumf1o  12444  fsumcvg2  12448  isummulc2  12473  fsum2dlem  12481  fsumcom2  12485  fsumshftm  12491  fsum0diag2  12493  fsum00  12504  fsumrlim  12517  o1fsum  12519  isumshft  12546  dvdsprm  13026  pythagtriplem4  13120  pcmptdvds  13190  proplem  13842  prslem  14315  posi  14334  clatlem  14466  dlatmjdi  14547  laspwcl  14593  lanfwcl  14594  mndlem1  14621  ghmlin  14938  cntzmhm2  15065  dprdss  15514  dprd2d2  15529  lmodlema  15882  islmodd  15883  lsscl  15946  lsslss  15964  lspdisjb  16125  rrgeq0i  16276  assalem  16303  ssnei2  17103  t1ficld  17313  t1sep2  17355  uncon  17413  1stcclb  17428  ptbasfi  17534  tx1stc  17603  qtoptop2  17652  r0sep  17701  ustincl  18158  ustdiag  18159  ustinvel  18160  ustexhalf  18161  prdsdsf  18305  prdsxmet  18307  cncfi  18795  ovolfiniun  19264  mbfimaopnlem  19414  limciun  19648  dvcn  19674  dvmptfsum  19726  dvfsumle  19772  dvfsumabs  19774  dvfsumlem3  19779  itgsubst  19800  fsumvma  20864  dchrelbasd  20890  dchrisumlem3  21052  usgranloop0  21266  nbgrassovt  21313  4cycl4dv  21502  grpoass  21639  ghomlin  21800  ghgrplem2  21803  rngodi  21821  rngodir  21822  rngoass  21823  lnolin  22103  elnlfn  23279  strlem4  23605  hstrlem4  23613  atmd  23750  esumcvg  24272  measxun2  24358  cvmcov  24729  ghomgrpilem1  24875  clim2prod  24995  ntrivcvgfvn0  25006  zprod  25042  fprod  25046  fprodf1o  25051  prodss  25052  fprodser  25054  fprodm1s  25072  fprodp1s  25073  fprodabs  25076  fprodefsum  25077  dfon2lem5  25167  frrlem4  25308  nofulllem5  25384  axcontlem9  25625  ifscgr  25692  nn0prpw  26017  neibastop2lem  26080  totbndss  26177  rngohomadd  26276  rngohommul  26277  crngocom  26302  idladdcl  26320  idllmulcl  26321  idlrmulcl  26322  elrfirn2  26441  wepwsolem  26807  kelac1  26830  islssfg2  26838  lnmlssfg  26847  lsslinds  26970  bnj110  28567  bnj594  28621  bnj1491  28764  oposlem  29298  cvlexch1  29443  hlsuprexch  29495  lautle  30198
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