New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > impbii | Unicode version |
Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
impbii.1 | |
impbii.2 |
Ref | Expression |
---|---|
impbii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbii.1 | . 2 | |
2 | impbii.2 | . 2 | |
3 | bi3 179 | . 2 | |
4 | 1, 2, 3 | mp2 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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: dfbi1 184 bicom 191 biid 227 2th 230 pm5.74 235 bitri 240 notnot 282 con34b 283 notbi 286 bibi2i 304 con1b 323 con2b 324 bi2.04 350 pm5.4 351 imdi 352 pm4.8 354 pm4.81 355 orcom 376 dfor2 400 impexp 433 ancom 437 oridm 500 orbi2i 505 or12 509 pm4.45im 545 pm4.44 560 pm4.79 566 anass 630 jaob 758 jcab 833 andi 837 pm4.72 846 oibabs 851 pm4.82 894 consensus 925 rnlem 931 3jaob 1244 truan 1331 dfnot 1332 3impexp 1366 3impexpbicom 1367 cad1 1398 tbw-bijust 1463 tbw-negdf 1464 19.26 1593 sbbii 1653 19.9v 1664 equcom 1680 ax12b 1689 19.3vOLD 1696 cbvalw 1701 cbvalvw 1702 alcom 1737 19.9hOLD 1781 19.3 1785 19.23hOLD 1820 equsalhwOLD 1839 19.21hOLD 1840 excomOLD 1859 19.41 1879 ax12olem1 1927 ax12olem3 1929 equsal 1960 cbval 1984 equs45f 1989 equvin 2001 sb6f 2039 dfsb2 2055 sbn 2062 sbim 2065 sb5rf 2090 sb6rf 2091 sb8 2092 sb9 2095 mo 2226 eu2 2229 mo2 2233 exmoeu 2246 euan 2261 2mo 2282 2eu6 2289 axext4 2337 cleqh 2450 nebi 2587 r19.26 2746 ralcom3 2776 ceqsex 2893 gencbvex 2901 gencbvex2 2902 eqvinc 2966 pm13.183 2979 rr19.3v 2980 rr19.28v 2981 euxfr2 3021 reu6 3025 reu3 3026 sbnfc2 3196 sspss 3368 unineq 3505 uneqin 3506 undif3 3515 difrab 3529 compleqb 3543 un00 3586 ssdifeq0 3632 r19.2zb 3640 ralf0 3656 elpr2 3752 snidb 3759 difsnb 3850 pwpw0 3855 sssn 3864 pwsnALT 3882 unissint 3950 uniintsn 3963 iununi 4050 unipw 4117 sspwb 4118 pwadjoin 4119 preq12b 4127 pw10b 4166 pw1disj 4167 pw1exb 4326 pw1equn 4331 pw1eqadj 4332 sspw1 4335 sspw12 4336 nnc0suc 4412 lefinlteq 4463 phi11 4596 phi011 4599 opth 4602 opexb 4603 ssopab2b 4713 ssrel 4844 xpid11 4926 iss 5000 xpnz 5045 ssrnres 5059 cnveqb 5063 cnvtr 5098 cnvexb 5103 dfxp2 5113 fn0 5202 funssxp 5233 f00 5249 dffo2 5273 ffoss 5314 f1o00 5317 fo00 5318 fv3 5341 dffn5 5363 dff2 5419 dff3 5420 dffo4 5423 dffo5 5424 ffnfv 5427 fsn 5432 fsn2 5434 fconstfv 5456 isores1 5494 eqfnov2 5590 fmpt 5692 brtxp 5783 op1st2nd 5790 clos1basesuc 5882 map0 6025 mapsn 6026 ensym 6037 en0 6042 enpw1 6062 mucnc 6131 1cnc 6139 dflec3 6221 nclenc 6222 lenc 6223 ncfin 6247 |
Copyright terms: Public domain | W3C validator |