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

Theorem pm2.43d 50
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 53 and pm2.43i 49. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43d.1 (𝜑 → (𝜓 → (𝜓𝜒)))
Assertion
Ref Expression
pm2.43d (𝜑 → (𝜓𝜒))

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
2 pm2.43d.1 . 2 (𝜑 → (𝜓 → (𝜓𝜒)))
31, 2mpdi 43 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  loolin  108  rspct  3274  po2nr  4961  somo  4982  ordelord  5647  tz7.7  5651  funssres  5829  2elresin  5901  dffv2  6165  f1imass  6399  onint  6864  wfrlem12  7290  wfrlem14  7292  onfununi  7302  smoel  7321  tfrlem11  7348  tfr3  7359  omass  7524  nnmass  7568  sbthlem1  7932  php  8006  inf3lem2  8386  cardne  8651  dfac2  8813  indpi  9585  genpcd  9684  ltexprlem7  9720  addcanpr  9724  reclem4pr  9728  suplem2pr  9731  sup2  10830  nnunb  11137  uzwo  11585  xrub  11972  grpid  17228  lsmcss  19802  uniopn  20474  fclsss1  21583  fclsss2  21584  0clwlk  26086  frg2wot1  26377  grpoid  26551  spansncvi  27688  pjnormssi  28204  sumdmdlem2  28455  trpredrec  30775  frrlem11  30829  sltval2  30846  nobndup  30892  nobnddown  30893  meran1  31373  poimirlem31  32393  heicant  32397  hlhilhillem  36053  ee223  37663  eel2122old  37747  afv0nbfvbi  39664  frgr2wwlk1  41475
  Copyright terms: Public domain W3C validator