![]() |
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 2767 eqvincg 2863 ddifstab 3269 csbprc 3470 undif4 3487 eqifdc 3571 sssnm 3756 sneqbg 3765 opthpr 3774 elpwuni 3978 ss1o0el1 4199 exmid01 4200 exmidundif 4208 eusv2i 4457 reusv3 4462 iunpw 4482 suc11g 4558 ssxpbm 5066 ssxp1 5067 ssxp2 5068 xp11m 5069 2elresin 5329 mpteqb 5608 f1fveq 5775 f1elima 5776 f1imass 5777 fliftf 5802 nnsucuniel 6498 iserd 6563 ecopovtrn 6634 ecopover 6635 ecopovtrng 6637 ecopoverg 6638 map0g 6690 fopwdom 6838 f1finf1o 6948 mkvprop 7158 addcanpig 7335 mulcanpig 7336 srpospr 7784 readdcan 8099 cnegexlem1 8134 addcan 8139 addcan2 8140 neg11 8210 negreb 8224 add20 8433 cru 8561 mulcanapd 8620 uz11 9552 eqreznegel 9616 lbzbi 9618 xneg11 9836 xnn0xadd0 9869 xsubge0 9883 elioc2 9938 elico2 9939 elicc2 9940 fzopth 10063 2ffzeq 10143 flqidz 10288 addmodlteq 10400 frec2uzrand 10407 expcan 10698 nn0opthd 10704 fz1eqb 10772 cj11 10916 sqrt0 11015 recan 11120 0dvds 11820 dvds1 11861 alzdvds 11862 nn0enne 11909 nn0oddm1d2 11916 nnoddm1d2 11917 divalgmod 11934 gcdeq0 11980 algcvgblem 12051 prmexpb 12153 ennnfonelemim 12427 grprcan 12915 grplcan 12937 grpinv11 12944 tgdom 13611 en1top 13616 hmeocnvb 13857 metrest 14045 lgsne0 14478 2lgsoddprmlem3 14498 bj-nnbist 14535 bj-nnbidc 14548 bj-peano4 14746 bj-nn0sucALT 14769 |
Copyright terms: Public domain | W3C validator |