![]() |
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 591 mtbid 596 mtbii 598 orbi2d 703 pm4.55dc 845 pm3.11dc 863 prlem1 879 nfimd 1474 dral1 1615 cbvalh 1633 ax16i 1735 speiv 1739 a16g 1741 cleqh 2134 pm13.18 2280 rspcimdv 2651 rspcimedv 2652 rspcedv 2654 moi2 2716 moi 2718 eqrd 2957 ralxfrd 4160 ralxfr2d 4162 rexxfr2d 4163 elres 4589 2elresin 4953 f1ocnv 5082 tz6.12c 5146 fvun1 5182 dffo4 5258 isores3 5398 tposfo2 5823 issmo2 5845 iordsmo 5853 smoel2 5859 prarloclemarch 6401 genprndl 6504 genprndu 6505 ltpopr 6569 ltsopr 6570 recexprlem1ssl 6605 recexprlem1ssu 6606 aptiprlemu 6612 lttrsr 6690 nnmulcl 7716 nnnegz 8024 eluzdc 8323 negm 8326 iccid 8564 icoshft 8628 fzen 8677 elfz2nn0 8743 elfzom1p1elfzo 8840 bj-omssind 9394 bj-bdfindes 9409 bj-nntrans 9411 bj-nnelirr 9413 bj-omtrans 9416 setindis 9427 bdsetindis 9429 bj-inf2vnlem3 9432 bj-inf2vnlem4 9433 bj-findis 9439 bj-findes 9441 |
Copyright terms: Public domain | W3C validator |