![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61d2 | Structured version Visualization version GIF version |
Description: Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
pm2.61d2.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
pm2.61d2.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
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 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 |