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 346 | . 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 372 imnan 438 annim 441 anor 510 pm4.53 513 pm4.55 515 oran 517 3ianor 1055 nanan 1449 xnor 1466 xorneg 1476 alnex 1706 exnal 1754 2exnexn 1772 equs3 1875 19.3v 1897 nne 2798 rexnal 2995 dfrex2 2996 r2exlem 3059 r19.35 3084 ddif 3742 dfun2 3859 dfin2 3860 difin 3861 dfnul2 3917 rab0OLD 3956 disj4 4025 snnzb 4254 onuninsuci 7040 omopthi 7737 dfsup2 8350 rankxplim3 8744 alephgeom 8905 fin1a2lem7 9228 fin41 9266 reclem2pr 9870 1re 10039 ltnlei 10158 divalglem8 15123 f1omvdco3 17869 elcls 20877 ist1-2 21151 fin1aufil 21736 dchrelbas3 24963 tgdim01 25402 axcontlem12 25855 avril1 27319 dftr6 31640 sltval2 31809 sltres 31815 nosepeq 31835 nolt02o 31845 nosupbnd2lem1 31861 dfon3 31999 dffun10 32021 brub 32061 bj-exnalimn 32610 bj-modal4e 32705 con2bii2 33180 heiborlem1 33610 heiborlem6 33615 heiborlem8 33617 cdleme0nex 35577 wopprc 37597 1nevenALTV 41602 |
Copyright terms: Public domain | W3C validator |