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

Theorem pm2.61d2 183
 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 181 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  185  jaoi  853  nfald2  2467  2ax6elem  2493  nfsbd  2564  sbal1  2572  nfabd2  2996  nfabd2OLD  2997  rgen2a  3216  posn  5609  frsn  5611  relimasn  5924  nfriotadw  7095  nfriotad  7098  tfinds  7548  curry1val  7774  curry2val  7778  onfununi  7952  findcard2s  8733  xpfi  8763  fiint  8769  acndom  9451  dfac12k  9547  iundom2g  9936  nqereu  10325  ltapr  10441  xrmax1  12543  xrmin2  12546  max1ALT  12554  hasheq0  13705  swrdnd2  13993  cshw1  14160  bezout  15865  ptbasfi  22161  filconn  22463  pcopt  23602  ioorinv  24155  itg1addlem2  24276  itg1addlem4  24278  itgss  24390  bddmulibl  24417  pthdlem2  27532  mdsymlem6  30166  sumdmdlem2  30177  bj-ax6elem1  34003  wl-equsb4  34830  wl-sbalnae  34835  poimirlem13  34942  poimirlem25  34954  poimirlem27  34956  remulid2  39382  sbgoldbaltlem1  44085  setrec2fun  44978
 Copyright terms: Public domain W3C validator