Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimprd | Unicode version |
Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Ref | Expression |
---|---|
biimprd.1 |
Ref | Expression |
---|---|
biimprd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | biimprd.1 | . 2 | |
3 | 1, 2 | syl5ibr 155 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl6bir 163 mpbird 166 sylibrd 168 sylbird 169 imbi1d 230 biimpar 295 mtbid 662 mtbii 664 orbi2d 780 pm4.55dc 927 pm3.11dc 946 prlem1 962 nfimd 1572 dral1 1717 cbvalv1 1738 cbvalh 1740 ax16i 1845 speiv 1849 a16g 1851 cbvalvw 1906 cbvexvw 1907 cleqh 2264 pm13.18 2415 rspcimdv 2826 rspcimedv 2827 rspcedv 2829 moi2 2902 moi 2904 eqrd 3155 abnexg 4418 ralxfrd 4434 ralxfr2d 4436 rexxfr2d 4437 elres 4914 2elresin 5293 f1ocnv 5439 tz6.12c 5510 fvun1 5546 dffo4 5627 isores3 5777 tposfo2 6226 issmo2 6248 iordsmo 6256 smoel2 6262 fiintim 6885 ismkvnex 7110 prarloclemarch 7350 genprndl 7453 genprndu 7454 ltpopr 7527 ltsopr 7528 recexprlem1ssl 7565 recexprlem1ssu 7566 aptiprlemu 7572 lttrsr 7694 nnmulcl 8869 nnnegz 9185 eluzdc 9539 negm 9544 iccid 9852 icoshft 9917 fzen 9968 elfz2nn0 10037 elfzom1p1elfzo 10139 flqeqceilz 10243 zmodidfzoimp 10279 caucvgre 10909 qdenre 11130 dvdsval2 11716 negdvdsb 11733 muldvds2 11743 dvdsabseq 11770 bezoutlemaz 11921 bezoutlembz 11922 rplpwr 11945 alginv 11958 algfx 11963 coprmgcdb 11999 divgcdcoprm0 12012 prmgt1 12043 oddprmgt2 12045 rpexp1i 12065 2sqpwodd 12087 qnumdencl 12098 phiprmpw 12133 prmdiveq 12147 prm23lt5 12174 pcmpt 12252 oddennn 12268 nninfdclemf1 12330 cnpnei 12766 bl2in 12950 addcncntoplem 13098 rescncf 13115 limcresi 13182 cnplimcim 13183 efltlemlt 13242 ioocosf1o 13322 uzdcinzz 13520 bj-charfunbi 13534 bj-omssind 13658 bj-bdfindes 13672 bj-nntrans 13674 bj-nnelirr 13676 bj-omtrans 13679 setindis 13690 bdsetindis 13692 bj-inf2vnlem3 13695 bj-inf2vnlem4 13696 bj-findis 13702 bj-findes 13704 |
Copyright terms: Public domain | W3C validator |