![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.24d | Structured version Visualization version GIF version |
Description: Deduction form of pm2.24 124. (Contributed by NM, 30-Jan-2006.) |
Ref | Expression |
---|---|
pm2.24d.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
pm2.24d | ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.24d.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) |
3 | 2 | con1d 145 | 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.5g 168 impimprbi 828 asymref2 6076 xpexr 7860 bropopvvv 8027 bropfvvvv 8029 reldmtpos 8170 zeo 12596 rpneg 12954 xrlttri 13065 difreicc 13408 pfxnd0 14583 nn0o1gt2 16270 cshwshashlem1 16975 gsumcom3fi 19763 gsumbagdiagOLD 21357 psrass1lemOLD 21358 gsumbagdiag 21360 psrass1lem 21361 cfinufil 23295 2sq2 26797 2sqnn0 26802 sltlpss 27258 sizusglecusg 28453 iswspthsnon 28843 clwlkclwwlklem2a4 28983 frgrncvvdeqlem8 29292 chirredi 31378 gsummpt2co 31932 truae 32882 bj-sngltag 35483 itg2addnclem 36158 itg2addnclem3 36160 cdleme32e 38937 dflim5 41693 ntrneiiso 42437 tz6.12-afv 45479 tz6.12-afv2 45546 odz2prm2pw 45829 lighneallem3 45873 lighneallem4b 45875 lindslinindsimp2lem5 46617 nnolog2flm1 46750 2itscp 46941 |
Copyright terms: Public domain | W3C validator |