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

Theorem mpd3an3 1280
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
Ref Expression
mpd3an3.2  |-  ( (
ph  /\  ps )  ->  ch )
mpd3an3.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mpd3an3  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mpd3an3
StepHypRef Expression
1 mpd3an3.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 mpd3an3.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1153 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpdan 650 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  elovmpt2  6230  f1oeng  7062  wdomimag  7488  cdaval  7983  gruuni  8608  genpv  8809  infmssuzle  10490  fzrevral3  11063  subsq2  11416  brfi1ind  11643  caubnd  12089  dvdsmul1  12798  dvdsmul2  12799  hashbcval  13297  setsvalg  13419  ressval  13443  restval  13581  latjle12  14418  latlem12  14434  lublem  14472  clatglb  14478  mrelatglb0  14538  imasmnd2  14659  divsinv  14926  ghminv  14940  symgov  15027  gexod  15147  lsmvalx  15200  rngrz  15628  imasrng  15652  irredneg  15742  ocvin  16824  restin  17152  qtopval  17648  elqtop3  17656  elfm3  17903  flimval  17916  nmge0  18534  nmeq0  18535  nminv  18538  nmo0  18640  0nghm  18646  evlrhm  19813  coemulhi  20039  isosctrlem2  20530  divsqrsumlem  20685  elghomlem1  21797  rngorz  21838  nvge0  22011  nvnd  22028  dip0r  22064  dip0l  22065  nmoo0  22140  hi2eq  22455  unitdivcld  24103  ltflcei  25950  lxflflp1  25952  rngonegmn1l  26256  rngonegmn1r  26257  igenval  26362  pellfund14  26652  mendmulr  27165  fmuldfeq  27381  stoweidlem19  27436  stoweidlem26  27443  lfl0  29180  op0le  29301  ople1  29306  olj01  29340  olm11  29342  atl0le  29419  hl2at  29519  pmapeq0  29880  trlcl  30278  trlle  30298  tendoid  30887  tendo0plr  30906  tendoipl2  30912  erngmul  30920  erngmul-rN  30928  dvamulr  31126  dvavadd  31129  dvhmulr  31201  cdlemm10N  31233
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  df-3an 938
  Copyright terms: Public domain W3C validator