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 646 mtbii 648 orbi2d 764 pm4.55dc 907 pm3.11dc 926 prlem1 942 nfimd 1549 dral1 1693 cbvalh 1711 ax16i 1814 speiv 1818 a16g 1820 cleqh 2217 pm13.18 2366 rspcimdv 2764 rspcimedv 2765 rspcedv 2767 moi2 2838 moi 2840 eqrd 3085 abnexg 4337 ralxfrd 4353 ralxfr2d 4355 rexxfr2d 4356 elres 4825 2elresin 5204 f1ocnv 5348 tz6.12c 5419 fvun1 5455 dffo4 5536 isores3 5684 tposfo2 6132 issmo2 6154 iordsmo 6162 smoel2 6168 fiintim 6785 ismkvnex 6997 prarloclemarch 7194 genprndl 7297 genprndu 7298 ltpopr 7371 ltsopr 7372 recexprlem1ssl 7409 recexprlem1ssu 7410 aptiprlemu 7416 lttrsr 7538 nnmulcl 8709 nnnegz 9025 eluzdc 9372 negm 9375 iccid 9676 icoshft 9741 fzen 9791 elfz2nn0 9860 elfzom1p1elfzo 9959 flqeqceilz 10059 zmodidfzoimp 10095 caucvgre 10721 qdenre 10942 dvdsval2 11423 negdvdsb 11436 muldvds2 11446 dvdsabseq 11472 bezoutlemaz 11618 bezoutlembz 11619 rplpwr 11642 alginv 11655 algfx 11660 coprmgcdb 11696 divgcdcoprm0 11709 prmgt1 11739 oddprmgt2 11741 rpexp1i 11759 2sqpwodd 11781 qnumdencl 11792 phiprmpw 11825 oddennn 11832 cnpnei 12315 bl2in 12499 addcncntoplem 12647 rescncf 12664 limcresi 12731 cnplimcim 12732 uzdcinzz 12932 bj-omssind 13060 bj-bdfindes 13074 bj-nntrans 13076 bj-nnelirr 13078 bj-omtrans 13081 setindis 13092 bdsetindis 13094 bj-inf2vnlem3 13097 bj-inf2vnlem4 13098 bj-findis 13104 bj-findes 13106 |
Copyright terms: Public domain | W3C validator |