![]() |
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 172 | 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 178 jaoi 888 nfald2 2466 nfsbd 2577 2ax6elem 2583 sbal1 2593 sbal2OLD 2595 nfabd2 2989 rgen2a 3186 posn 5422 frsn 5424 relimasn 5729 nfriotad 6874 tfinds 7320 curry1val 7534 curry2val 7538 onfununi 7704 findcard2s 8470 xpfi 8500 fiint 8506 acndom 9187 dfac12k 9284 iundom2g 9677 nqereu 10066 ltapr 10182 xrmax1 12294 xrmin2 12297 max1ALT 12305 hasheq0 13444 swrdnd2 13720 cshw1 13943 bezout 15633 ptbasfi 21755 filconn 22057 pcopt 23191 ioorinv 23742 itg1addlem2 23863 itg1addlem4 23865 itgss 23977 bddmulibl 24004 pthdlem2 27070 mdsymlem6 29811 sumdmdlem2 29822 bj-ax6elem1 33180 wl-equsb4 33876 wl-sbalnae 33882 poimirlem13 33959 poimirlem25 33971 poimirlem27 33973 sbgoldbaltlem1 42490 setrec2fun 43327 |
Copyright terms: Public domain | W3C validator |