![]() |
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 7318 omopthi 8021 dfsup2 8638 rankxplim3 9041 alephgeom 9238 fin1a2lem7 9563 fin41 9601 reclem2pr 10205 1re 10376 ltnlei 10497 divalglem8 15530 f1omvdco3 18252 elcls 21285 ist1-2 21559 fin1aufil 22144 dchrelbas3 25415 tgdim01 25858 axcontlem12 26324 avril1 27894 dftr6 32234 sltval2 32398 sltres 32404 nosepeq 32424 nolt02o 32434 nosupbnd2lem1 32450 dfon3 32588 dffun10 32610 brub 32650 bj-exnalimn 33189 bj-modal4e 33293 con2bii2 33776 wl-dfrexf 33980 wl-dfrexv 33982 wl-dfrexex 33983 wl-dfrexsb 33984 heiborlem1 34234 heiborlem6 34239 heiborlem8 34241 cdleme0nex 36444 wopprc 38556 1nevenALTV 42627 |
Copyright terms: Public domain | W3C validator |