|   | 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 6136 xpexr 7941 bropopvvv 8116 bropfvvvv 8118 reldmtpos 8260 zeo 12706 rpneg 13068 xrlttri 13182 difreicc 13525 pfxnd0 14727 nn0o1gt2 16419 cshwshashlem1 17134 gsumcom3fi 19998 gsumbagdiag 21952 psrass1lem 21953 cfinufil 23937 2sq2 27478 2sqnn0 27483 sltlpss 27946 sizusglecusg 29482 iswspthsnon 29877 clwlkclwwlklem2a4 30017 frgrncvvdeqlem8 30326 chirredi 32414 gsummpt2co 33052 truae 34245 bj-sngltag 36985 itg2addnclem 37679 itg2addnclem3 37681 cdleme32e 40448 dflim5 43347 ntrneiiso 44109 tz6.12-afv 47190 tz6.12-afv2 47257 odz2prm2pw 47555 lighneallem3 47599 lighneallem4b 47601 lindslinindsimp2lem5 48384 nnolog2flm1 48516 2itscp 48707 oppcmndclem 48920 | 
| Copyright terms: Public domain | W3C validator |