![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 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 293 notbid 633 mtbid 638 mtbii 640 orbi2d 745 pm4.55dc 890 pm3.11dc 909 prlem1 925 nfimd 1532 dral1 1676 cbvalh 1694 ax16i 1797 speiv 1801 a16g 1803 cleqh 2199 pm13.18 2348 rspcimdv 2745 rspcimedv 2746 rspcedv 2748 moi2 2818 moi 2820 eqrd 3065 abnexg 4305 ralxfrd 4321 ralxfr2d 4323 rexxfr2d 4324 elres 4791 2elresin 5170 f1ocnv 5314 tz6.12c 5383 fvun1 5419 dffo4 5500 isores3 5648 tposfo2 6094 issmo2 6116 iordsmo 6124 smoel2 6130 fiintim 6746 prarloclemarch 7127 genprndl 7230 genprndu 7231 ltpopr 7304 ltsopr 7305 recexprlem1ssl 7342 recexprlem1ssu 7343 aptiprlemu 7349 lttrsr 7458 nnmulcl 8599 nnnegz 8909 eluzdc 9254 negm 9257 iccid 9549 icoshft 9614 fzen 9664 elfz2nn0 9733 elfzom1p1elfzo 9832 flqeqceilz 9932 zmodidfzoimp 9968 caucvgre 10593 qdenre 10814 dvdsval2 11291 negdvdsb 11304 muldvds2 11314 dvdsabseq 11340 bezoutlemaz 11484 bezoutlembz 11485 rplpwr 11508 alginv 11521 algfx 11526 coprmgcdb 11562 divgcdcoprm0 11575 prmgt1 11605 oddprmgt2 11607 rpexp1i 11625 2sqpwodd 11646 qnumdencl 11657 phiprmpw 11690 oddennn 11697 cnpnei 12169 bl2in 12331 rescncf 12481 limcresi 12515 cnplimcim 12516 uzdcinzz 12586 bj-omssind 12718 bj-bdfindes 12732 bj-nntrans 12734 bj-nnelirr 12736 bj-omtrans 12739 setindis 12750 bdsetindis 12752 bj-inf2vnlem3 12755 bj-inf2vnlem4 12756 bj-findis 12762 bj-findes 12764 |
Copyright terms: Public domain | W3C validator |