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

Theorem pm2.61d2 172
Description: Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
pm2.61d2.1 (𝜑 → (¬ 𝜓𝜒))
pm2.61d2.2 (𝜓𝜒)
Assertion
Ref Expression
pm2.61d2 (𝜑𝜒)

Proof of Theorem pm2.61d2
StepHypRef Expression
1 pm2.61d2.2 . . 3 (𝜓𝜒)
21a1i 11 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61d2.1 . 2 (𝜑 → (¬ 𝜓𝜒))
42, 3pm2.61d 170 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61ii  177  jaoi  394  nfald2  2330  nfsbd  2441  2ax6elem  2448  sbal1  2459  sbal2  2460  nfabd2  2780  rgen2a  2972  posn  5153  frsn  5155  relimasn  5452  nfriotad  6579  tfinds  7013  curry1val  7222  curry2val  7226  onfununi  7390  findcard2s  8152  xpfi  8182  fiint  8188  acndom  8825  dfac12k  8920  iundom2g  9313  nqereu  9702  ltapr  9818  xrmax1  11956  xrmin2  11959  max1ALT  11967  hasheq0  13101  swrdnd2  13378  cshw1  13512  bezout  15191  ptbasfi  21303  filconn  21606  pcopt  22741  ioorinv  23263  itg1addlem2  23383  itg1addlem4  23385  itgss  23497  bddmulibl  23524  pthdlem2  26546  mdsymlem6  29134  sumdmdlem2  29145  bj-ax6elem1  32320  wl-equsb4  32997  wl-sbalnae  33004  poimirlem13  33081  poimirlem25  33093  poimirlem27  33095  sgoldbaltlem1  40983  setrec2fun  41753
  Copyright terms: Public domain W3C validator