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

Theorem mpd3an3 1463
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 1119 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 686 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  stoic2b  1778  elovmpo  7603  f1oeng  8918  php  9161  nnsdomg  9253  wdomimag  9530  gruuni  10743  genpv  10942  pncan3  11416  mulsubaddmulsub  11626  infssuzle  12863  fzrevral3  13535  flflp1  13719  subsq2  14122  brfi1ind  14405  opfi1ind  14408  ccatws1ls  14528  swrdrlen  14554  pfxpfxid  14604  pfxcctswrd  14605  2cshwid  14709  caubnd  15250  dvdsmul1  16167  dvdsmul2  16168  hashbcval  16881  setsvalg  17045  ressval  17122  restval  17315  mrelatglb0  18457  imasmnd2  18600  efmndov  18698  qusinv  18996  ghminv  19022  gsmsymgrfixlem1  19216  gsmsymgreqlem2  19220  gexod  19375  lsmvalx  19428  ringrz  20019  imasring  20052  irredneg  20148  ocvin  21094  frlmiscvec  21271  evlrhm  21522  gsumsmonply1  21690  mat1mhm  21849  marrepfval  21925  marrepval0  21926  marepvfval  21930  marepvval0  21931  1elcpmat  22080  m2cpminv0  22126  idpm2idmp  22166  chfacfscmulgsum  22225  chfacfpmmulgsum  22229  restin  22533  qtopval  23062  elqtop3  23070  elfm3  23317  flimval  23330  nmge0  23989  nmeq0  23990  nminv  23993  nmo0  24115  0nghm  24121  coemulhi  25631  isosctrlem2  26185  divsqrtsumlem  26345  2lgsoddprmlem4  26779  0uhgrrusgr  28568  frgruhgr0v  29250  nvge0  29657  nvnd  29672  dip0r  29701  dip0l  29702  nmoo0  29775  hi2eq  30089  wrdsplex  31836  resvval  32158  unitdivcld  32522  signspval  33204  satfv0  33992  ltflcei  36095  elghomlem1OLD  36373  rngorz  36411  rngonegmn1l  36429  rngonegmn1r  36430  igenval  36549  xrnidresex  36898  xrncnvepresex  36899  lfl0  37556  olj01  37716  olm11  37718  hl2at  37897  pmapeq0  38258  trlcl  38656  trlle  38676  tendoid  39265  tendo0plr  39284  tendoipl2  39290  erngmul  39298  erngmul-rN  39306  dvamulr  39504  dvavadd  39507  dvhmulr  39578  cdlemm10N  39610  repncan3  40881  pellfund14  41250  mendmulr  41544  onnog  41775  fmuldfeq  43898  stoweidlem19  44334  stoweidlem26  44341  addsubeq0  45602  prelspr  45752  lincval1  46574
  Copyright terms: Public domain W3C validator