![]() |
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 214 | . . 3 ⊢ (¬ 𝜓 ↔ 𝜑) |
3 | 2 | con1bii 345 | . 2 ⊢ (¬ 𝜑 ↔ 𝜓) |
4 | 3 | bicomi 214 | 1 ⊢ (𝜓 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: xor3 371 imnan 386 annim 390 anor 957 pm4.53 960 pm4.55 962 oran 964 3ianorOLD 1098 nanan 1597 xnor 1614 xorneg 1624 alnex 1854 exnal 1902 2exnexn 1922 equs3 2044 19.3v 2066 nne 2947 rexnal 3143 dfrex2 3144 r2exlem 3207 r19.35 3232 ddif 3894 dfun2 4009 dfin2 4010 difin 4011 dfnul2 4066 disj4 4170 snnzb 4391 onuninsuci 7188 omopthi 7892 dfsup2 8507 rankxplim3 8909 alephgeom 9106 fin1a2lem7 9431 fin41 9469 reclem2pr 10073 1re 10242 ltnlei 10361 divalglem8 15332 f1omvdco3 18077 elcls 21099 ist1-2 21373 fin1aufil 21957 dchrelbas3 25185 tgdim01 25624 axcontlem12 26077 avril1 27662 dftr6 31979 sltval2 32147 sltres 32153 nosepeq 32173 nolt02o 32183 nosupbnd2lem1 32199 dfon3 32337 dffun10 32359 brub 32399 bj-exnalimn 32948 bj-modal4e 33043 con2bii2 33518 heiborlem1 33943 heiborlem6 33948 heiborlem8 33950 cdleme0nex 36100 wopprc 38124 1nevenALTV 42131 |
Copyright terms: Public domain | W3C validator |