![]() |
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 2485 reubida 2672 rmobida 2677 mpteq12f 4101 reuhypd 4492 funbrfv2b 5584 dffn5im 5585 eqfnfv2 5638 fndmin 5647 fniniseg 5660 rexsupp 5664 fmptco 5706 dff13 5793 riotabidva 5872 mpoeq123dva 5961 mpoeq3dva 5964 mpoxopovel 6270 qliftfun 6647 erovlem 6657 xpcomco 6856 pw2f1odclem 6866 elfi2 7005 ctssdccl 7144 ltexpi 7371 dfplpq2 7388 axprecex 7914 zrevaddcl 9338 qrevaddcl 9680 icoshft 10026 fznn 10125 shftdm 10872 2shfti 10881 sumeq2 11408 fsum3 11436 fsum2dlemstep 11483 prodeq2 11606 fprodseq 11632 gcdaddm 12026 grpidpropdg 12861 ismgmid 12864 gsumpropd2 12879 mhmpropd 12941 issubm2 12948 eqgid 13190 eqgabl 13292 rngpropd 13334 iscrng2 13394 ringpropd 13417 crngpropd 13418 crngunit 13486 dvdsrpropdg 13522 issubrg3 13619 lsslss 13722 lsspropdg 13772 bastop2 14069 restopn2 14168 iscnp3 14188 lmbr2 14199 txlm 14264 ismet2 14339 xblpnfps 14383 xblpnf 14384 blininf 14409 blres 14419 elmopn2 14434 neibl 14476 metrest 14491 metcnp3 14496 metcnp 14497 metcnp2 14498 metcn 14499 txmetcn 14504 cnbl0 14519 cnblcld 14520 bl2ioo 14527 elcncf2 14546 cncfmet 14564 cnlimc 14626 |
Copyright terms: Public domain | W3C validator |