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

Step	Hyp	Ref	Expression
1		pm2.61d2.2	. . 3 ⊢ (𝜓 → 𝜒)
2	1	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61d2.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
4	2, 3	pm2.61d 181	1 ⊢ (𝜑 → 𝜒)

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  3004  nfabd2OLD  3005  rgen2a  3231  posn  5639  frsn  5641  relimasn  5954  nfriotadw  7124  nfriotad  7127  tfinds  7576  curry1val  7802  curry2val  7806  onfununi  7980  findcard2s  8761  xpfi  8791  fiint  8797  acndom  9479  dfac12k  9575  iundom2g  9964  nqereu  10353  ltapr  10469  xrmax1  12571  xrmin2  12574  max1ALT  12582  hasheq0  13727  swrdnd2  14019  cshw1  14186  bezout  15893  ptbasfi  22191  filconn  22493  pcopt  23628  ioorinv  24179  itg1addlem2  24300  itg1addlem4  24302  itgss  24414  bddmulibl  24441  pthdlem2  27551  mdsymlem6  30187  sumdmdlem2  30198  bj-ax6elem1  34001  wl-equsb4  34795  wl-sbalnae  34800  poimirlem13  34907  poimirlem25  34919  poimirlem27  34921  remulid2  39256  sbgoldbaltlem1  43951  setrec2fun  44802