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

Theorem mpd3an3 1573
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 1111 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 667 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  stoic2b  1848  elovmpt2  7029  f1oeng  8131  wdomimag  8651  cdaval  9197  gruuni  9827  genpv  10026  infssuzle  11978  fzrevral3  12633  flflp1  12815  subsq2  13179  brfi1ind  13482  opfi1ind  13485  ccatws1ls  13617  swrdrlen  13643  swrd0swrdid  13672  2cshwid  13768  caubnd  14305  dvdsmul1  15211  dvdsmul2  15212  hashbcval  15912  setsvalg  16093  ressval  16133  restval  16294  mrelatglb0  17392  imasmnd2  17534  qusinv  17860  ghminv  17874  symgov  18016  gexod  18207  lsmvalx  18260  ringrz  18795  imasring  18826  irredneg  18917  evlrhm  19739  gsumsmonply1  19887  ocvin  20234  frlmiscvec  20404  mat1mhm  20507  marrepfval  20583  marrepval0  20584  marepvfval  20588  marepvval0  20589  1elcpmat  20739  m2cpminv0  20785  idpm2idmp  20825  chfacfscmulgsum  20884  chfacfpmmulgsum  20888  restin  21190  qtopval  21718  elqtop3  21726  elfm3  21973  flimval  21986  nmge0  22640  nmeq0  22641  nminv  22644  nmo0  22758  0nghm  22764  coemulhi  24229  isosctrlem2  24769  divsqrtsumlem  24926  2lgsoddprmlem4  25360  0uhgrrusgr  26708  frgruhgr0v  27444  nvge0  27867  nvnd  27882  dip0r  27911  dip0l  27912  nmoo0  27985  hi2eq  28301  resvval  30166  unitdivcld  30286  signspval  30968  ltflcei  33729  elghomlem1OLD  34015  rngorz  34053  rngonegmn1l  34071  rngonegmn1r  34072  igenval  34191  xrnidresex  34506  xrncnvepresex  34507  lfl0  34873  olj01  35033  olm11  35035  hl2at  35213  pmapeq0  35574  trlcl  35973  trlle  35993  tendoid  36582  tendo0plr  36601  tendoipl2  36607  erngmul  36615  erngmul-rN  36623  dvamulr  36821  dvavadd  36824  dvhmulr  36896  cdlemm10N  36928  pellfund14  37988  mendmulr  38284  fmuldfeq  40330  stoweidlem19  40750  stoweidlem26  40757  pfxpfxid  41941  pfxcctswrd  41942  prelspr  42261  lincval1  42733
  Copyright terms: Public domain W3C validator