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

Theorem mpd3an3 1459
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 1115 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 686 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  stoic2b  1777  elovmpo  7373  f1oeng  8511  wdomimag  9035  gruuni  10207  genpv  10406  pncan3  10879  mulsubaddmulsub  11089  infssuzle  12317  fzrevral3  12987  flflp1  13170  subsq2  13567  brfi1ind  13851  opfi1ind  13854  ccatws1ls  13981  swrdrlen  14010  pfxpfxid  14060  pfxcctswrd  14061  2cshwid  14165  caubnd  14707  dvdsmul1  15620  dvdsmul2  15621  hashbcval  16325  setsvalg  16501  ressval  16540  restval  16689  mrelatglb0  17784  imasmnd2  17937  efmndov  18035  qusinv  18328  ghminv  18354  gsmsymgrfixlem1  18544  gsmsymgreqlem2  18548  gexod  18700  lsmvalx  18753  ringrz  19327  imasring  19358  irredneg  19449  evlrhm  20295  gsumsmonply1  20457  ocvin  20804  frlmiscvec  20979  mat1mhm  21079  marrepfval  21155  marrepval0  21156  marepvfval  21160  marepvval0  21161  1elcpmat  21309  m2cpminv0  21355  idpm2idmp  21395  chfacfscmulgsum  21454  chfacfpmmulgsum  21458  restin  21760  qtopval  22289  elqtop3  22297  elfm3  22544  flimval  22557  nmge0  23212  nmeq0  23213  nminv  23216  nmo0  23330  0nghm  23336  coemulhi  24840  isosctrlem2  25394  divsqrtsumlem  25554  2lgsoddprmlem4  25988  0uhgrrusgr  27357  frgruhgr0v  28038  nvge0  28445  nvnd  28460  dip0r  28489  dip0l  28490  nmoo0  28563  hi2eq  28877  wrdsplex  30611  resvval  30918  unitdivcld  31162  signspval  31840  satfv0  32623  ltflcei  34945  elghomlem1OLD  35223  rngorz  35261  rngonegmn1l  35279  rngonegmn1r  35280  igenval  35399  xrnidresex  35715  xrncnvepresex  35716  lfl0  36261  olj01  36421  olm11  36423  hl2at  36601  pmapeq0  36962  trlcl  37360  trlle  37380  tendoid  37969  tendo0plr  37988  tendoipl2  37994  erngmul  38002  erngmul-rN  38010  dvamulr  38208  dvavadd  38211  dvhmulr  38282  cdlemm10N  38314  repncan3  39372  pellfund14  39671  mendmulr  39964  fmuldfeq  42067  stoweidlem19  42503  stoweidlem26  42510  addsubeq0  43695  prelspr  43845  lincval1  44669
  Copyright terms: Public domain W3C validator