![]() |
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 3568 sssnm 3752 sneqbg 3761 opthpr 3770 elpwuni 3973 ss1o0el1 4194 exmid01 4195 exmidundif 4203 eusv2i 4452 reusv3 4457 iunpw 4477 suc11g 4553 ssxpbm 5060 ssxp1 5061 ssxp2 5062 xp11m 5063 2elresin 5323 mpteqb 5602 f1fveq 5767 f1elima 5768 f1imass 5769 fliftf 5794 nnsucuniel 6490 iserd 6555 ecopovtrn 6626 ecopover 6627 ecopovtrng 6629 ecopoverg 6630 map0g 6682 fopwdom 6830 f1finf1o 6940 mkvprop 7150 addcanpig 7321 mulcanpig 7322 srpospr 7770 readdcan 8084 cnegexlem1 8119 addcan 8124 addcan2 8125 neg11 8195 negreb 8209 add20 8418 cru 8546 mulcanapd 8604 uz11 9536 eqreznegel 9600 lbzbi 9602 xneg11 9818 xnn0xadd0 9851 xsubge0 9865 elioc2 9920 elico2 9921 elicc2 9922 fzopth 10044 2ffzeq 10124 flqidz 10269 addmodlteq 10381 frec2uzrand 10388 expcan 10677 nn0opthd 10683 fz1eqb 10751 cj11 10895 sqrt0 10994 recan 11099 0dvds 11799 dvds1 11839 alzdvds 11840 nn0enne 11887 nn0oddm1d2 11894 nnoddm1d2 11895 divalgmod 11912 gcdeq0 11958 algcvgblem 12029 prmexpb 12131 ennnfonelemim 12405 grprcan 12797 grplcan 12818 grpinv11 12825 tgdom 13232 en1top 13237 hmeocnvb 13478 metrest 13666 lgsne0 14099 bj-nnbist 14145 bj-nnbidc 14158 bj-peano4 14356 bj-nn0sucALT 14379 |
Copyright terms: Public domain | W3C validator |