![]() |
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 443 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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: rexbida 2406 reubida 2586 rmobida 2591 mpteq12f 3968 reuhypd 4352 funbrfv2b 5420 dffn5im 5421 eqfnfv2 5473 fndmin 5481 fniniseg 5494 rexsupp 5498 fmptco 5540 dff13 5623 riotabidva 5700 mpoeq123dva 5786 mpoeq3dva 5789 mpoxopovel 6092 qliftfun 6465 erovlem 6475 xpcomco 6673 elfi2 6812 ctssdccl 6948 ltexpi 7090 dfplpq2 7107 axprecex 7612 zrevaddcl 9005 qrevaddcl 9335 icoshft 9663 fznn 9759 shftdm 10484 2shfti 10493 sumeq2 11017 fsum3 11045 fsum2dlemstep 11092 gcdaddm 11517 bastop2 12093 restopn2 12192 iscnp3 12211 lmbr2 12222 txlm 12287 ismet2 12340 xblpnfps 12384 xblpnf 12385 blininf 12410 blres 12420 elmopn2 12435 neibl 12477 metrest 12492 metcnp3 12497 metcnp 12498 metcnp2 12499 metcn 12500 txmetcn 12505 cnbl0 12520 cnblcld 12521 bl2ioo 12525 elcncf2 12544 cncfmet 12562 cnlimc 12594 |
Copyright terms: Public domain | W3C validator |