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 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 661 mtbii 663 orbi2d 779 pm4.55dc 922 pm3.11dc 941 prlem1 957 nfimd 1564 dral1 1708 cbvalh 1726 ax16i 1830 speiv 1834 a16g 1836 cleqh 2239 pm13.18 2389 rspcimdv 2790 rspcimedv 2791 rspcedv 2793 moi2 2865 moi 2867 eqrd 3115 abnexg 4367 ralxfrd 4383 ralxfr2d 4385 rexxfr2d 4386 elres 4855 2elresin 5234 f1ocnv 5380 tz6.12c 5451 fvun1 5487 dffo4 5568 isores3 5716 tposfo2 6164 issmo2 6186 iordsmo 6194 smoel2 6200 fiintim 6817 ismkvnex 7029 prarloclemarch 7226 genprndl 7329 genprndu 7330 ltpopr 7403 ltsopr 7404 recexprlem1ssl 7441 recexprlem1ssu 7442 aptiprlemu 7448 lttrsr 7570 nnmulcl 8741 nnnegz 9057 eluzdc 9404 negm 9407 iccid 9708 icoshft 9773 fzen 9823 elfz2nn0 9892 elfzom1p1elfzo 9991 flqeqceilz 10091 zmodidfzoimp 10127 caucvgre 10753 qdenre 10974 dvdsval2 11496 negdvdsb 11509 muldvds2 11519 dvdsabseq 11545 bezoutlemaz 11691 bezoutlembz 11692 rplpwr 11715 alginv 11728 algfx 11733 coprmgcdb 11769 divgcdcoprm0 11782 prmgt1 11812 oddprmgt2 11814 rpexp1i 11832 2sqpwodd 11854 qnumdencl 11865 phiprmpw 11898 oddennn 11905 cnpnei 12388 bl2in 12572 addcncntoplem 12720 rescncf 12737 limcresi 12804 cnplimcim 12805 uzdcinzz 13005 bj-omssind 13133 bj-bdfindes 13147 bj-nntrans 13149 bj-nnelirr 13151 bj-omtrans 13154 setindis 13165 bdsetindis 13167 bj-inf2vnlem3 13170 bj-inf2vnlem4 13171 bj-findis 13177 bj-findes 13179 |
Copyright terms: Public domain | W3C validator |