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  393  nfald2  2362  nfsbd  2470  2ax6elem  2477  sbal1  2488  sbal2  2489  nfabd2  2813  rgen2a  3006  posn  5221  frsn  5223  relimasn  5523  nfriotad  6659  tfinds  7101  curry1val  7315  curry2val  7319  onfununi  7483  findcard2s  8242  xpfi  8272  fiint  8278  acndom  8912  dfac12k  9007  iundom2g  9400  nqereu  9789  ltapr  9905  xrmax1  12044  xrmin2  12047  max1ALT  12055  hasheq0  13192  swrdnd2  13479  cshw1  13614  bezout  15307  ptbasfi  21432  filconn  21734  pcopt  22868  ioorinv  23390  itg1addlem2  23509  itg1addlem4  23511  itgss  23623  bddmulibl  23650  pthdlem2  26720  mdsymlem6  29395  sumdmdlem2  29406  bj-ax6elem1  32776  wl-equsb4  33468  wl-sbalnae  33475  poimirlem13  33552  poimirlem25  33564  poimirlem27  33566  sbgoldbaltlem1  41992  setrec2fun  42764
  Copyright terms: Public domain W3C validator