| 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 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 870 nfald2 2479 2ax6elem 2504 nfsbd 2556 sbal1 2562 nfabd2 2950 rgen2a 3361 posn 5738 frsn 5740 relimasn 6078 nfriotadw 7365 nfriotad 7368 tfinds 7844 curry1val 8088 curry2val 8092 onfununi 8316 findcard2s 9138 prfi 9271 fiint 9274 acndom 10023 dfac12k 10119 iundom2g 10512 nqereu 10902 ltapr 11018 xrmax1 13192 xrmin2 13195 max1ALT 13203 hasheq0 14390 swrdnd2 14683 cshw1 14849 bezout 16591 ptbasfi 23699 filconn 24001 pcopt 25142 ioorinv 25696 itg1addlem2 25817 itg1addlem4 25819 itgss 25932 bddmulibl 25959 maxs1 27891 mins2 27894 pthdlem2 30026 mdsymlem6 32669 sumdmdlem2 32680 vonf1oonfo 35470 bj-ax6elem1 37150 wl-equsb4 38072 wl-sbalnae 38077 poimirlem13 38144 poimirlem25 38156 poimirlem27 38158 remullid 43055 sbgoldbaltlem1 48399 setrec2fun 50321 |
| Copyright terms: Public domain | W3C validator |