New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > con2bii | GIF version |
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
con2bii.1 | ⊢ (φ ↔ ¬ ψ) |
Ref | Expression |
---|---|
con2bii | ⊢ (ψ ↔ ¬ φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2bii.1 | . . . 4 ⊢ (φ ↔ ¬ ψ) | |
2 | 1 | bicomi 193 | . . 3 ⊢ (¬ ψ ↔ φ) |
3 | 2 | con1bii 321 | . 2 ⊢ (¬ φ ↔ ψ) |
4 | 3 | bicomi 193 | 1 ⊢ (ψ ↔ ¬ φ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 176 |
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 177 |
This theorem is referenced by: xor3 346 imnan 411 annim 414 anor 475 pm4.53 478 pm4.55 480 oran 482 3ianor 949 nanan 1289 xnor 1306 xorass 1308 xorneg1 1311 xorneg 1313 alnex 1543 exnal 1574 2exnexn 1580 equs3 1644 19.3v 1665 19.9vOLD 1697 equsex 1962 nne 2520 dfral2 2626 dfrex2 2627 r19.35 2758 elin 3219 dblcompl 3227 ddif 3398 dfun2 3490 dfin2 3491 difin 3492 dfnul2 3552 rab0 3571 disj4 3599 dfimak2 4298 dfint3 4318 dfpw2 4327 dfaddc2 4381 nndisjeq 4429 ltfinex 4464 ssfin 4470 tfinltfin 4501 evenfinex 4503 oddfinex 4504 evenoddnnnul 4514 evenodddisjlem1 4515 setconslem2 4732 setconslem3 4733 setconslem7 4737 dfswap2 4741 imasn 5018 brimage 5793 releqmpt2 5809 disjex 5823 funsex 5828 transex 5910 refex 5911 antisymex 5912 connexex 5913 foundex 5914 extex 5915 symex 5916 ltcirr 6272 |
Copyright terms: Public domain | W3C validator |