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 181
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 179 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  183  jaoi  856  nfald2  2444  2ax6elem  2469  nfsbd  2521  sbal1  2528  nfabd2  2930  rgen2a  3343  posn  5718  frsn  5720  relimasn  6037  nfriotadw  7322  nfriotad  7326  tfinds  7797  curry1val  8038  curry2val  8042  onfununi  8288  findcard2s  9112  xpfiOLD  9265  fiint  9271  acndom  9992  dfac12k  10088  iundom2g  10481  nqereu  10870  ltapr  10986  xrmax1  13100  xrmin2  13103  max1ALT  13111  hasheq0  14269  swrdnd2  14549  cshw1  14716  bezout  16429  ptbasfi  22948  filconn  23250  pcopt  24401  ioorinv  24956  itg1addlem2  25077  itg1addlem4  25079  itg1addlem4OLD  25080  itgss  25192  bddmulibl  25219  maxs1  27129  mins2  27132  pthdlem2  28758  mdsymlem6  31392  sumdmdlem2  31403  bj-ax6elem1  35176  wl-equsb4  36058  wl-sbalnae  36063  poimirlem13  36137  poimirlem25  36149  poimirlem27  36151  remulid2  40945  sbgoldbaltlem1  46057  setrec2fun  47223
  Copyright terms: Public domain W3C validator