![]() |
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 129 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: impbid2 143 iba 300 ibar 301 pm4.81dc 909 pm5.63dc 948 pm4.83dc 953 pm5.71dc 963 19.33b2 1640 19.9t 1653 sb4b 1845 a16gb 1876 euor2 2096 eupickbi 2120 ceqsalg 2780 eqvincg 2876 ddifstab 3282 csbprc 3483 undif4 3500 eqifdc 3584 sssnm 3769 sneqbg 3778 opthpr 3787 elpwuni 3991 ss1o0el1 4215 exmid01 4216 exmidundif 4224 eusv2i 4473 reusv3 4478 iunpw 4498 suc11g 4574 ssxpbm 5082 ssxp1 5083 ssxp2 5084 xp11m 5085 2elresin 5346 mpteqb 5627 f1fveq 5794 f1elima 5795 f1imass 5796 fliftf 5821 nnsucuniel 6521 iserd 6586 ecopovtrn 6659 ecopover 6660 ecopovtrng 6662 ecopoverg 6663 map0g 6715 fopwdom 6865 f1finf1o 6977 mkvprop 7187 addcanpig 7364 mulcanpig 7365 srpospr 7813 readdcan 8128 cnegexlem1 8163 addcan 8168 addcan2 8169 neg11 8239 negreb 8253 add20 8462 cru 8590 mulcanapd 8649 uz11 9582 eqreznegel 9646 lbzbi 9648 xneg11 9866 xnn0xadd0 9899 xsubge0 9913 elioc2 9968 elico2 9969 elicc2 9970 fzopth 10093 2ffzeq 10173 flqidz 10319 addmodlteq 10431 frec2uzrand 10438 expcan 10731 nn0opthd 10737 fz1eqb 10805 cj11 10949 sqrt0 11048 recan 11153 0dvds 11853 dvds1 11894 alzdvds 11895 nn0enne 11942 nn0oddm1d2 11949 nnoddm1d2 11950 divalgmod 11967 gcdeq0 12013 algcvgblem 12084 prmexpb 12186 4sqexercise2 12434 4sqlemsdc 12435 4sqlem11 12436 ennnfonelemim 12478 grprcan 12996 grplcan 13021 grpinv11 13028 tgdom 14049 en1top 14054 hmeocnvb 14295 metrest 14483 lgsne0 14917 2lgsoddprmlem3 14937 bj-nnbist 14974 bj-nnbidc 14987 bj-peano4 15185 bj-nn0sucALT 15208 |
Copyright terms: Public domain | W3C validator |