![]() |
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 855 nfald2 2438 2ax6elem 2463 nfsbd 2515 sbal1 2521 nfabd2 2918 rgen2a 3354 posn 5763 frsn 5765 relimasn 6089 nfriotadw 7383 nfriotad 7387 tfinds 7865 curry1val 8110 curry2val 8114 onfununi 8362 findcard2s 9190 xpfiOLD 9344 fiint 9350 acndom 10076 dfac12k 10172 iundom2g 10565 nqereu 10954 ltapr 11070 xrmax1 13189 xrmin2 13192 max1ALT 13200 hasheq0 14358 swrdnd2 14641 cshw1 14808 bezout 16522 ptbasfi 23529 filconn 23831 pcopt 24993 ioorinv 25549 itg1addlem2 25670 itg1addlem4 25672 itg1addlem4OLD 25673 itgss 25785 bddmulibl 25812 maxs1 27744 mins2 27747 pthdlem2 29654 mdsymlem6 32290 sumdmdlem2 32301 bj-ax6elem1 36273 wl-equsb4 37155 wl-sbalnae 37160 poimirlem13 37237 poimirlem25 37249 poimirlem27 37251 remullid 42123 sbgoldbaltlem1 47256 setrec2fun 48309 |
Copyright terms: Public domain | W3C validator |