Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimprd | GIF 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 145 | 1 ⊢ (𝜑 → (𝜒 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: syl6bir 153 mpbird 156 sylibrd 158 sylbird 159 imbi1d 220 biimpar 281 notbid 592 mtbid 597 mtbii 599 orbi2d 704 pm4.55dc 846 pm3.11dc 864 prlem1 880 nfimd 1477 dral1 1618 cbvalh 1636 ax16i 1738 speiv 1742 a16g 1744 cleqh 2137 pm13.18 2286 rspcimdv 2657 rspcimedv 2658 rspcedv 2660 moi2 2722 moi 2724 eqrd 2963 ralxfrd 4194 ralxfr2d 4196 rexxfr2d 4197 elres 4646 2elresin 5010 f1ocnv 5139 tz6.12c 5203 fvun1 5239 dffo4 5315 isores3 5455 tposfo2 5882 issmo2 5904 iordsmo 5912 smoel2 5918 prarloclemarch 6516 genprndl 6619 genprndu 6620 ltpopr 6693 ltsopr 6694 recexprlem1ssl 6731 recexprlem1ssu 6732 aptiprlemu 6738 lttrsr 6847 nnmulcl 7935 nnnegz 8248 eluzdc 8547 negm 8550 iccid 8794 icoshft 8858 fzen 8907 elfz2nn0 8973 elfzom1p1elfzo 9070 flqeqceilz 9160 caucvgre 9580 qdenre 9798 ialginv 9886 ialgfx 9891 bj-omssind 10059 bj-bdfindes 10074 bj-nntrans 10076 bj-nnelirr 10078 bj-omtrans 10081 setindis 10092 bdsetindis 10094 bj-inf2vnlem3 10097 bj-inf2vnlem4 10098 bj-findis 10104 bj-findes 10106 |
Copyright terms: Public domain | W3C validator |