![]() |
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-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 mtbid 644 mtbii 646 orbi2d 762 pm4.55dc 905 pm3.11dc 924 prlem1 940 nfimd 1547 dral1 1691 cbvalh 1709 ax16i 1812 speiv 1816 a16g 1818 cleqh 2214 pm13.18 2363 rspcimdv 2761 rspcimedv 2762 rspcedv 2764 moi2 2834 moi 2836 eqrd 3081 abnexg 4327 ralxfrd 4343 ralxfr2d 4345 rexxfr2d 4346 elres 4813 2elresin 5192 f1ocnv 5336 tz6.12c 5405 fvun1 5441 dffo4 5522 isores3 5670 tposfo2 6118 issmo2 6140 iordsmo 6148 smoel2 6154 fiintim 6770 ismkvnex 6979 prarloclemarch 7174 genprndl 7277 genprndu 7278 ltpopr 7351 ltsopr 7352 recexprlem1ssl 7389 recexprlem1ssu 7390 aptiprlemu 7396 lttrsr 7505 nnmulcl 8651 nnnegz 8961 eluzdc 9306 negm 9309 iccid 9601 icoshft 9666 fzen 9716 elfz2nn0 9785 elfzom1p1elfzo 9884 flqeqceilz 9984 zmodidfzoimp 10020 caucvgre 10645 qdenre 10866 dvdsval2 11344 negdvdsb 11357 muldvds2 11367 dvdsabseq 11393 bezoutlemaz 11537 bezoutlembz 11538 rplpwr 11561 alginv 11574 algfx 11579 coprmgcdb 11615 divgcdcoprm0 11628 prmgt1 11658 oddprmgt2 11660 rpexp1i 11678 2sqpwodd 11699 qnumdencl 11710 phiprmpw 11743 oddennn 11750 cnpnei 12230 bl2in 12392 addcncntoplem 12537 rescncf 12554 limcresi 12591 cnplimcim 12592 uzdcinzz 12697 bj-omssind 12825 bj-bdfindes 12839 bj-nntrans 12841 bj-nnelirr 12843 bj-omtrans 12846 setindis 12857 bdsetindis 12859 bj-inf2vnlem3 12862 bj-inf2vnlem4 12863 bj-findis 12869 bj-findes 12871 |
Copyright terms: Public domain | W3C validator |