![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con2bii | Structured version Visualization version GIF version |
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
con2bii.1 | ⊢ (𝜑 ↔ ¬ 𝜓) |
Ref | Expression |
---|---|
con2bii | ⊢ (𝜓 ↔ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2bii.1 | . . . 4 ⊢ (𝜑 ↔ ¬ 𝜓) | |
2 | 1 | bicomi 216 | . . 3 ⊢ (¬ 𝜓 ↔ 𝜑) |
3 | 2 | con1bii 348 | . 2 ⊢ (¬ 𝜑 ↔ 𝜓) |
4 | 3 | bicomi 216 | 1 ⊢ (𝜓 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 |
This theorem is referenced by: xor3 374 imnan 390 annim 394 anor 968 pm4.53 971 pm4.55 973 oran 975 nanan 1559 xnor 1584 xorneg 1594 alnex 1825 exnal 1870 2exnexn 1890 equs3 2006 19.3v 2031 nne 2973 rexnal 3176 dfrex2 3177 r2exlem 3244 r19.35 3270 ddif 3965 dfun2 4086 dfin2 4087 difin 4088 dfnul2OLD 4144 disj4 4251 snnzb 4485 onuninsuci 7320 omopthi 8023 dfsup2 8640 rankxplim3 9043 alephgeom 9240 fin1a2lem7 9565 fin41 9603 reclem2pr 10207 1re 10378 ltnlei 10499 divalglem8 15540 f1omvdco3 18263 elcls 21296 ist1-2 21570 fin1aufil 22155 dchrelbas3 25426 tgdim01 25875 axcontlem12 26341 avril1 27911 dftr6 32242 sltval2 32406 sltres 32412 nosepeq 32432 nolt02o 32442 nosupbnd2lem1 32458 dfon3 32596 dffun10 32618 brub 32658 bj-exnalimn 33197 bj-modal4e 33301 con2bii2 33783 wl-dfrexf 33989 wl-dfrexv 33991 wl-dfrexex 33992 wl-dfrexsb 33993 heiborlem1 34243 heiborlem6 34248 heiborlem8 34250 cdleme0nex 36453 wopprc 38570 1nevenALTV 42641 |
Copyright terms: Public domain | W3C validator |