![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm5.32d 450 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: rexbida 2482 reubida 2669 rmobida 2674 mpteq12f 4095 reuhypd 4483 funbrfv2b 5573 dffn5im 5574 eqfnfv2 5627 fndmin 5636 fniniseg 5649 rexsupp 5653 fmptco 5695 dff13 5782 riotabidva 5860 mpoeq123dva 5949 mpoeq3dva 5952 mpoxopovel 6255 qliftfun 6630 erovlem 6640 xpcomco 6839 elfi2 6984 ctssdccl 7123 ltexpi 7349 dfplpq2 7366 axprecex 7892 zrevaddcl 9316 qrevaddcl 9657 icoshft 10003 fznn 10102 shftdm 10844 2shfti 10853 sumeq2 11380 fsum3 11408 fsum2dlemstep 11455 prodeq2 11578 fprodseq 11604 gcdaddm 11998 grpidpropdg 12811 ismgmid 12814 mhmpropd 12876 issubm2 12883 eqgid 13115 iscrng2 13252 ringpropd 13275 crngpropd 13276 crngunit 13343 dvdsrpropdg 13379 issubrg3 13431 lsslss 13534 lsspropdg 13584 bastop2 13824 restopn2 13923 iscnp3 13943 lmbr2 13954 txlm 14019 ismet2 14094 xblpnfps 14138 xblpnf 14139 blininf 14164 blres 14174 elmopn2 14189 neibl 14231 metrest 14246 metcnp3 14251 metcnp 14252 metcnp2 14253 metcn 14254 txmetcn 14259 cnbl0 14274 cnblcld 14275 bl2ioo 14282 elcncf2 14301 cncfmet 14319 cnlimc 14381 |
Copyright terms: Public domain | W3C validator |