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  3005  vtocl3gf  3006  vtoclegft  3015  sbcthdv  3168  swopolem  4504  peano5  4859  funssres  5484  dffv2  5787  fmptcof  5893  fnpr  5941  fnprOLD  5942  fliftfuns  6027  isorel  6037  caovclg  6230  caovcomg  6233  caovassg  6236  caovcang  6239  caovordig  6243  caovordg  6245  caovdig  6252  caovdirg  6255  qliftfuns  6982  nneneq  7281  cfslb  8135  hsmexlem4  8298  axdc3lem2  8320  axdc4lem  8324  adderpq  8822  mulerpq  8823  ltordlem  9541  lble  9949  uz11  10497  xrsupsslem  10874  xrinfmsslem  10875  xrsupss  10876  xrinfmss  10877  fseqsupubi  11305  hashbclem  11689  isercolllem1  12446  caucvgb  12461  zsum  12500  fsum  12502  fsumf1o  12505  fsumcvg2  12509  isummulc2  12534  fsum2dlem  12542  fsumcom2  12546  fsumshftm  12552  fsum0diag2  12554  fsum00  12565  fsumrlim  12578  o1fsum  12580  isumshft  12607  dvdsprm  13087  pythagtriplem4  13181  pcmptdvds  13251  proplem  13903  prslem  14376  posi  14395  clatlem  14527  dlatmjdi  14608  laspwcl  14654  lanfwcl  14655  mndlem1  14682  ghmlin  14999  cntzmhm2  15126  dprdss  15575  dprd2d2  15590  lmodlema  15943  islmodd  15944  lsscl  16007  lsslss  16025  lspdisjb  16186  rrgeq0i  16337  assalem  16364  ssnei2  17168  t1ficld  17379  t1sep2  17421  uncon  17480  1stcclb  17495  ptbasfi  17601  tx1stc  17670  qtoptop2  17719  r0sep  17768  ustincl  18225  ustdiag  18226  ustinvel  18227  ustexhalf  18228  psmet0  18327  psmettri2  18328  prdsdsf  18385  prdsxmet  18387  cncfi  18912  ovolfiniun  19385  mbfimaopnlem  19535  limciun  19769  dvcn  19795  dvmptfsum  19847  dvfsumle  19893  dvfsumabs  19895  dvfsumlem3  19900  itgsubst  19921  fsumvma  20985  dchrelbasd  21011  dchrisumlem3  21173  usgranloop0  21388  nbgrassovt  21435  4cycl4dv  21642  grpoass  21779  ghomlin  21940  ghgrplem2  21943  rngodi  21961  rngodir  21962  rngoass  21963  lnolin  22243  elnlfn  23419  strlem4  23745  hstrlem4  23753  atmd  23890  esumcvg  24464  measxun2  24552  sibfima  24641  cvmcov  24938  ghomgrpilem1  25084  clim2prod  25205  ntrivcvgfvn0  25216  zprod  25252  fprod  25256  fprodf1o  25261  prodss  25262  fprodser  25264  fprodm1s  25282  fprodp1s  25283  fprodabs  25286  fprodefsum  25287  fprod2dlem  25293  fprodcom2  25297  dfon2lem5  25398  frrlem4  25539  nofulllem5  25615  axcontlem9  25859  ifscgr  25926  mbfresfi  26199  nn0prpw  26263  neibastop2lem  26326  totbndss  26423  rngohomadd  26522  rngohommul  26523  crngocom  26548  idladdcl  26566  idllmulcl  26567  idlrmulcl  26568  elrfirn2  26687  wepwsolem  27053  kelac1  27076  islssfg2  27084  lnmlssfg  27093  lsslinds  27216  2elfz3nn0  28034  swrdswrd  28086  swrdccatin12b  28102  2shwrd2lem1a  28140  2shwrd2lem1  28142  usgra2wlkspthlem2  28181  bnj110  29083  bnj594  29137  bnj1491  29280  oposlem  29820  cvlexch1  29965  hlsuprexch  30017  lautle  30720
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