![]() |
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 908 pm5.63dc 946 pm4.83dc 951 pm5.71dc 961 19.33b2 1629 19.9t 1642 sb4b 1834 a16gb 1865 euor2 2084 eupickbi 2108 ceqsalg 2765 eqvincg 2861 ddifstab 3267 csbprc 3468 undif4 3485 eqifdc 3569 sssnm 3753 sneqbg 3762 opthpr 3771 elpwuni 3974 ss1o0el1 4195 exmid01 4196 exmidundif 4204 eusv2i 4453 reusv3 4458 iunpw 4478 suc11g 4554 ssxpbm 5061 ssxp1 5062 ssxp2 5063 xp11m 5064 2elresin 5324 mpteqb 5603 f1fveq 5768 f1elima 5769 f1imass 5770 fliftf 5795 nnsucuniel 6491 iserd 6556 ecopovtrn 6627 ecopover 6628 ecopovtrng 6630 ecopoverg 6631 map0g 6683 fopwdom 6831 f1finf1o 6941 mkvprop 7151 addcanpig 7328 mulcanpig 7329 srpospr 7777 readdcan 8091 cnegexlem1 8126 addcan 8131 addcan2 8132 neg11 8202 negreb 8216 add20 8425 cru 8553 mulcanapd 8612 uz11 9544 eqreznegel 9608 lbzbi 9610 xneg11 9828 xnn0xadd0 9861 xsubge0 9875 elioc2 9930 elico2 9931 elicc2 9932 fzopth 10054 2ffzeq 10134 flqidz 10279 addmodlteq 10391 frec2uzrand 10398 expcan 10687 nn0opthd 10693 fz1eqb 10761 cj11 10905 sqrt0 11004 recan 11109 0dvds 11809 dvds1 11849 alzdvds 11850 nn0enne 11897 nn0oddm1d2 11904 nnoddm1d2 11905 divalgmod 11922 gcdeq0 11968 algcvgblem 12039 prmexpb 12141 ennnfonelemim 12415 grprcan 12838 grplcan 12860 grpinv11 12867 tgdom 13354 en1top 13359 hmeocnvb 13600 metrest 13788 lgsne0 14221 bj-nnbist 14267 bj-nnbidc 14280 bj-peano4 14478 bj-nn0sucALT 14501 |
Copyright terms: Public domain | W3C validator |