Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.32da | Unicode version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.) |
Ref | Expression |
---|---|
pm5.32da.1 |
Ref | Expression |
---|---|
pm5.32da |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32da.1 | . . 3 | |
2 | 1 | ex 114 | . 2 |
3 | 2 | pm5.32d 445 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 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: rexbida 2430 reubida 2610 rmobida 2615 mpteq12f 4003 reuhypd 4387 funbrfv2b 5459 dffn5im 5460 eqfnfv2 5512 fndmin 5520 fniniseg 5533 rexsupp 5537 fmptco 5579 dff13 5662 riotabidva 5739 mpoeq123dva 5825 mpoeq3dva 5828 mpoxopovel 6131 qliftfun 6504 erovlem 6514 xpcomco 6713 elfi2 6853 ctssdccl 6989 ltexpi 7138 dfplpq2 7155 axprecex 7681 zrevaddcl 9097 qrevaddcl 9429 icoshft 9766 fznn 9862 shftdm 10587 2shfti 10596 sumeq2 11121 fsum3 11149 fsum2dlemstep 11196 prodeq2 11319 gcdaddm 11661 bastop2 12242 restopn2 12341 iscnp3 12361 lmbr2 12372 txlm 12437 ismet2 12512 xblpnfps 12556 xblpnf 12557 blininf 12582 blres 12592 elmopn2 12607 neibl 12649 metrest 12664 metcnp3 12669 metcnp 12670 metcnp2 12671 metcn 12672 txmetcn 12677 cnbl0 12692 cnblcld 12693 bl2ioo 12700 elcncf2 12719 cncfmet 12737 cnlimc 12799 |
Copyright terms: Public domain | W3C validator |