![]() |
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 6117 xpexr 7920 bropopvvv 8089 bropfvvvv 8091 reldmtpos 8233 zeo 12672 rpneg 13032 xrlttri 13144 difreicc 13487 pfxnd0 14664 nn0o1gt2 16351 cshwshashlem1 17058 gsumcom3fi 19927 gsumbagdiagOLD 21866 psrass1lemOLD 21867 gsumbagdiag 21869 psrass1lem 21870 cfinufil 23825 2sq2 27359 2sqnn0 27364 sltlpss 27826 sizusglecusg 29270 iswspthsnon 29660 clwlkclwwlklem2a4 29800 frgrncvvdeqlem8 30109 chirredi 32197 gsummpt2co 32756 truae 33856 bj-sngltag 36456 itg2addnclem 37138 itg2addnclem3 37140 cdleme32e 39912 dflim5 42752 ntrneiiso 43515 tz6.12-afv 46547 tz6.12-afv2 46614 odz2prm2pw 46897 lighneallem3 46941 lighneallem4b 46943 lindslinindsimp2lem5 47524 nnolog2flm1 47657 2itscp 47848 |
Copyright terms: Public domain | W3C validator |