MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpd3an3 Structured version   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  6283  f1oeng  7118  wdomimag  7547  cdaval  8042  gruuni  8667  genpv  8868  infmssuzle  10550  fzrevral3  11125  subsq2  11481  brfi1ind  11708  caubnd  12154  dvdsmul1  12863  dvdsmul2  12864  hashbcval  13362  setsvalg  13484  ressval  13508  restval  13646  latjle12  14483  latlem12  14499  lublem  14537  clatglb  14543  mrelatglb0  14603  imasmnd2  14724  divsinv  14991  ghminv  15005  symgov  15092  gexod  15212  lsmvalx  15265  rngrz  15693  imasrng  15717  irredneg  15807  ocvin  16893  restin  17222  qtopval  17719  elqtop3  17727  elfm3  17974  flimval  17987  nmge0  18655  nmeq0  18656  nminv  18659  nmo0  18761  0nghm  18767  evlrhm  19938  coemulhi  20164  isosctrlem2  20655  divsqrsumlem  20810  elghomlem1  21941  rngorz  21982  nvge0  22155  nvnd  22172  dip0r  22208  dip0l  22209  nmoo0  22284  hi2eq  22599  unitdivcld  24291  ltflcei  26231  lxflflp1  26233  rngonegmn1l  26556  rngonegmn1r  26557  igenval  26662  pellfund14  26952  mendmulr  27464  fmuldfeq  27680  stoweidlem19  27735  stoweidlem26  27742  swrdrlen  28156  addlenrevswrd  28157  cshwlen  28207  lfl0  29800  op0le  29921  ople1  29926  olj01  29960  olm11  29962  atl0le  30039  hl2at  30139  pmapeq0  30500  trlcl  30898  trlle  30918  tendoid  31507  tendo0plr  31526  tendoipl2  31532  erngmul  31540  erngmul-rN  31548  dvamulr  31746  dvavadd  31749  dvhmulr  31821  cdlemm10N  31853
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