![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imbi2d | GIF version |
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbid.1 | ⊢ (φ → (ψ ↔ χ)) |
Ref | Expression |
---|---|
imbi2d | ⊢ (φ → ((θ → ψ) ↔ (θ → χ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
2 | 1 | a1d 22 | . 2 ⊢ (φ → (θ → (ψ ↔ χ))) |
3 | 2 | pm5.74d 171 | 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: imbi12d 223 imbi2 226 pm5.42 303 imandc 785 pm4.14dc 786 imimorbdc 794 pm5.6dc 834 ax11v2 1698 ax11v 1705 equs5or 1708 mo23 1938 2gencl 2581 3gencl 2582 vtocl2gf 2609 vtocl3gf 2610 eqeu 2705 mo2icl 2714 euind 2722 reu7 2730 reuind 2738 sbctt 2818 sbcnestgf 2891 preq12bg 3535 elint 3612 elintrabg 3619 intab 3635 trss 3854 bm1.3ii 3869 pocl 4031 swopolem 4033 sowlin 4048 reusv3 4158 regexmid 4219 ordsoexmid 4240 tfisi 4253 finds2 4267 nnregexmid 4285 vtoclr 4331 2optocl 4360 3optocl 4361 raliunxp 4420 resieq 4565 iss 4597 cnveqb 4719 funmo 4860 fnbrfvb 5157 fvelimab 5172 fvmptssdm 5198 fmptco 5273 fnressn 5292 fressnfv 5293 isoselem 5402 isosolem 5406 ovg 5581 caovcan 5607 caovordig 5608 caovord 5614 f1o2ndf1 5791 poxp 5794 smoeq 5846 smores 5848 tfrlem1 5864 tfrlemi1 5887 tfrexlem 5889 tfri3 5894 rdgon 5913 freccl 5932 nnacl 5998 nnmcl 5999 nnacom 6002 nnaass 6003 nndi 6004 nnmass 6005 nnmsucr 6006 nnmcom 6007 nnsucsssuc 6010 nntri3or 6011 nnaordi 6017 nnaword 6020 nnmordi 6025 nnaordex 6036 2ecoptocl 6130 3ecoptocl 6131 th3qlem2 6145 xpdom2g 6242 distrnq0 6442 addassnq0 6445 elinp 6457 prcdnql 6467 prcunqu 6468 prarloclem3 6480 caucvgpr 6653 ltsosr 6692 pitonn 6744 axpre-ltwlin 6767 nnaddcl 7715 nnmulcl 7716 zaddcllempos 8058 zaddcllemneg 8060 prime 8113 peano5uzti 8122 uzind2 8126 zindd 8132 uzaddcl 8305 frec2uzltd 8870 frec2uzrdg 8876 frecuzrdgfn 8879 iseqfveq2 8905 expivallem 8910 expcllem 8920 expap0 8939 mulexp 8948 expadd 8951 expmul 8954 leexp2r 8962 leexp1a 8963 bernneq 9022 cjexp 9121 bdbm1.3ii 9346 bj-2inf 9397 bj-omtrans 9416 |
Copyright terms: Public domain | W3C validator |