![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > con2bii | Unicode 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 194 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | con1bii 322 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomi 194 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem is referenced by: xor3 347 imnan 412 annim 415 anor 476 pm4.53 479 pm4.55 481 oran 483 3ianor 951 nanan 1295 xnor 1312 xorass 1314 xorneg1 1317 xorneg 1319 alnex 1549 exnal 1580 2exnexn 1587 equs3 1651 19.3v 1673 19.9vOLD 1706 equsexOLD 1970 nne 2579 dfral2 2686 dfrex2 2687 r19.35 2823 ddif 3447 dfun2 3544 dfin2 3545 difin 3546 dfnul2 3598 rab0 3616 disj4 3644 onuninsuci 4787 omopthi 6867 dfsup2 7413 dfsup2OLD 7414 rankxplim3 7769 alephgeom 7927 fin1a2lem7 8250 fin41 8288 reclem2pr 8889 1re 9054 ltnlei 9158 divalglem8 12883 elcls 17100 ist1-2 17373 fin1aufil 17925 dchrelbas3 20983 avril1 21718 dftr6 25329 sltval2 25532 sltres 25540 nodenselem4 25560 nodenselem7 25563 nofulllem5 25582 dfon3 25654 dffun10 25675 elfuns 25676 axcontlem12 25826 heiborlem1 26418 heiborlem6 26423 heiborlem8 26425 wopprc 26999 f1omvdco3 27268 equsexNEW7 29208 cdleme0nex 30784 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 |
Copyright terms: Public domain | W3C validator |