![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impbid1 | Unicode version |
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
Ref | Expression |
---|---|
impbid1.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
impbid1.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
impbid1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbid1.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | impbid1.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | impbid 128 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: impbid2 142 iba 296 ibar 297 pm4.81dc 858 pm5.63dc 898 pm4.83dc 903 pm5.71dc 913 19.33b2 1576 19.9t 1589 sb4b 1773 a16gb 1804 euor2 2018 eupickbi 2042 ceqsalg 2669 eqvincg 2763 ddifstab 3155 csbprc 3355 undif4 3372 eqifdc 3453 sssnm 3628 sneqbg 3637 opthpr 3646 elpwuni 3848 exmid01 4061 exmidundif 4067 eusv2i 4314 reusv3 4319 iunpw 4339 suc11g 4410 ssxpbm 4910 ssxp1 4911 ssxp2 4912 xp11m 4913 2elresin 5170 mpteqb 5443 f1fveq 5605 f1elima 5606 f1imass 5607 fliftf 5632 nnsucuniel 6321 iserd 6385 ecopovtrn 6456 ecopover 6457 ecopovtrng 6459 ecopoverg 6460 map0g 6512 fopwdom 6659 f1finf1o 6763 mkvprop 6943 addcanpig 7043 mulcanpig 7044 srpospr 7478 readdcan 7773 cnegexlem1 7808 addcan 7813 addcan2 7814 neg11 7884 negreb 7898 add20 8103 cru 8230 mulcanapd 8283 uz11 9198 eqreznegel 9256 lbzbi 9258 xneg11 9458 xnn0xadd0 9491 xsubge0 9505 elioc2 9560 elico2 9561 elicc2 9562 fzopth 9682 2ffzeq 9759 flqidz 9900 addmodlteq 10012 frec2uzrand 10019 expcan 10304 nn0opthd 10309 fz1eqb 10378 cj11 10518 sqrt0 10616 recan 10721 0dvds 11308 dvds1 11346 alzdvds 11347 nn0enne 11394 nn0oddm1d2 11401 nnoddm1d2 11402 divalgmod 11419 gcdeq0 11460 algcvgblem 11523 prmexpb 11622 ennnfonelemim 11729 tgdom 12023 en1top 12028 metrest 12434 bj-peano4 12738 bj-nn0sucALT 12761 |
Copyright terms: Public domain | W3C validator |