MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan9 Structured version   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  3013  vtocl3gf  3014  vtoclegft  3023  sbcthdv  3176  swopolem  4512  peano5  4868  funssres  5493  dffv2  5796  fmptcof  5902  fnpr  5950  fnprOLD  5951  fliftfuns  6036  isorel  6046  caovclg  6239  caovcomg  6242  caovassg  6245  caovcang  6248  caovordig  6252  caovordg  6254  caovdig  6261  caovdirg  6264  qliftfuns  6991  nneneq  7290  cfslb  8146  hsmexlem4  8309  axdc3lem2  8331  axdc4lem  8335  adderpq  8833  mulerpq  8834  ltordlem  9552  lble  9960  uz11  10508  xrsupsslem  10885  xrinfmsslem  10886  xrsupss  10887  xrinfmss  10888  fseqsupubi  11317  hashbclem  11701  isercolllem1  12458  caucvgb  12473  zsum  12512  fsum  12514  fsumf1o  12517  fsumcvg2  12521  isummulc2  12546  fsum2dlem  12554  fsumcom2  12558  fsumshftm  12564  fsum0diag2  12566  fsum00  12577  fsumrlim  12590  o1fsum  12592  isumshft  12619  dvdsprm  13099  pythagtriplem4  13193  pcmptdvds  13263  proplem  13915  prslem  14388  posi  14407  clatlem  14539  dlatmjdi  14620  laspwcl  14666  lanfwcl  14667  mndlem1  14694  ghmlin  15011  cntzmhm2  15138  dprdss  15587  dprd2d2  15602  lmodlema  15955  islmodd  15956  lsscl  16019  lsslss  16037  lspdisjb  16198  rrgeq0i  16349  assalem  16376  ssnei2  17180  t1ficld  17391  t1sep2  17433  uncon  17492  1stcclb  17507  ptbasfi  17613  tx1stc  17682  qtoptop2  17731  r0sep  17780  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  psmet0  18339  psmettri2  18340  prdsdsf  18397  prdsxmet  18399  cncfi  18924  ovolfiniun  19397  mbfimaopnlem  19547  limciun  19781  dvcn  19807  dvmptfsum  19859  dvfsumle  19905  dvfsumabs  19907  dvfsumlem3  19912  itgsubst  19933  fsumvma  20997  dchrelbasd  21023  dchrisumlem3  21185  usgranloop0  21400  nbgrassovt  21447  4cycl4dv  21654  grpoass  21791  ghomlin  21952  ghgrplem2  21955  rngodi  21973  rngodir  21974  rngoass  21975  lnolin  22255  elnlfn  23431  strlem4  23757  hstrlem4  23765  atmd  23902  esumcvg  24476  measxun2  24564  sibfima  24653  cvmcov  24950  ghomgrpilem1  25096  clim2prod  25216  ntrivcvgfvn0  25227  zprod  25263  fprod  25267  fprodf1o  25272  prodss  25273  fprodser  25275  fprodm1s  25293  fprodp1s  25294  fprodabs  25297  fprodefsum  25298  fprod2dlem  25304  fprodcom2  25308  dfon2lem5  25414  frrlem4  25585  nofulllem5  25661  axcontlem9  25911  ifscgr  25978  mbfresfi  26253  nn0prpw  26326  neibastop2lem  26389  totbndss  26486  rngohomadd  26585  rngohommul  26586  crngocom  26611  idladdcl  26629  idllmulcl  26630  idlrmulcl  26631  elrfirn2  26750  wepwsolem  27116  kelac1  27138  islssfg2  27146  lnmlssfg  27155  lsslinds  27278  2elfz3nn0  28112  2elfz2melfz  28117  swrdswrd  28199  swrdccatin2  28210  2cshw2lem1  28252  usgra2wlkspthlem2  28307  bnj110  29229  bnj594  29283  bnj1491  29426  oposlem  29981  cvlexch1  30126  hlsuprexch  30178  lautle  30881
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