| 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 5737 frsn 5739 relimasn 6077 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 13189 xrmin2 13192 max1ALT 13200 hasheq0 14387 swrdnd2 14681 cshw1 14847 bezout 16589 ptbasfi 23695 filconn 23997 pcopt 25138 ioorinv 25692 itg1addlem2 25813 itg1addlem4 25815 itgss 25928 bddmulibl 25955 maxs1 27887 mins2 27890 pthdlem2 30022 mdsymlem6 32665 sumdmdlem2 32676 vonf1oonfo 35465 bj-ax6elem1 37145 wl-equsb4 38067 wl-sbalnae 38072 poimirlem13 38139 poimirlem25 38151 poimirlem27 38153 remullid 43050 sbgoldbaltlem1 48400 setrec2fun 50322 |
| Copyright terms: Public domain | W3C validator |