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

Theorem mpd3an3 1422
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
Ref Expression
mpd3an3.2 ((𝜑𝜓) → 𝜒)
mpd3an3.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mpd3an3 ((𝜑𝜓) → 𝜃)

Proof of Theorem mpd3an3
StepHypRef Expression
1 mpd3an3.2 . 2 ((𝜑𝜓) → 𝜒)
2 mpd3an3.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expa 1262 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 701 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  stoic2b  1697  elovmpt2  6839  f1oeng  7926  wdomimag  8444  cdaval  8944  gruuni  9574  genpv  9773  infssuzle  11723  fzrevral3  12376  flflp1  12556  subsq2  12921  brfi1ind  13228  opfi1ind  13231  brfi1indOLD  13234  opfi1indOLD  13237  ccatws1ls  13356  swrdrlen  13381  swrd0swrdid  13410  2cshwid  13505  caubnd  14040  dvdsmul1  14938  dvdsmul2  14939  hashbcval  15641  setsvalg  15819  ressval  15859  restval  16019  mrelatglb0  17117  imasmnd2  17259  qusinv  17585  ghminv  17599  symgov  17742  gexod  17933  lsmvalx  17986  ringrz  18520  imasring  18551  irredneg  18642  evlrhm  19457  gsumsmonply1  19605  ocvin  19950  frlmiscvec  20120  mat1mhm  20222  marrepfval  20298  marrepval0  20299  marepvfval  20303  marepvval0  20304  1elcpmat  20452  m2cpminv0  20498  idpm2idmp  20538  chfacfscmulgsum  20597  chfacfpmmulgsum  20601  restin  20893  qtopval  21421  elqtop3  21429  elfm3  21677  flimval  21690  nmge0  22344  nmeq0  22345  nminv  22348  nmo0  22462  0nghm  22468  coemulhi  23931  isosctrlem2  24466  divsqrtsumlem  24623  2lgsoddprmlem4  25057  0uhgrrusgr  26361  frgruhgr0v  27010  nvge0  27398  nvnd  27413  dip0r  27442  dip0l  27443  nmoo0  27516  hi2eq  27832  resvval  29636  unitdivcld  29753  signspval  30433  ltflcei  33064  elghomlem1OLD  33351  rngorz  33389  rngonegmn1l  33407  rngonegmn1r  33408  igenval  33527  lfl0  33867  olj01  34027  olm11  34029  hl2at  34206  pmapeq0  34567  trlcl  34966  trlle  34986  tendoid  35576  tendo0plr  35595  tendoipl2  35601  erngmul  35609  erngmul-rN  35617  dvamulr  35815  dvavadd  35818  dvhmulr  35890  cdlemm10N  35922  pellfund14  36977  mendmulr  37274  fmuldfeq  39247  stoweidlem19  39569  stoweidlem26  39576  pfxpfxid  40741  pfxcctswrd  40742  prelspr  41050  lincval1  41522
  Copyright terms: Public domain W3C validator