![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm5.32i | Unicode version |
Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
pm5.32i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm5.32i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm5.32 453 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 145 |
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: pm5.32ri 455 biadan2 456 anbi2i 457 abai 560 anabs5 573 pm5.33 609 eq2tri 2237 rexbiia 2492 reubiia 2661 rmobiia 2666 rabbiia 2722 ceqsrexbv 2868 euxfrdc 2923 eldifpr 3619 eldiftp 3638 eldifsn 3719 elrint 3884 elriin 3956 opeqsn 4251 rabxp 4662 eliunxp 4765 restidsing 4962 ressn 5168 fncnv 5281 dff1o5 5469 respreima 5643 dff4im 5661 dffo3 5662 f1ompt 5666 fsn 5687 fconst3m 5734 fconst4m 5735 eufnfv 5745 dff13 5766 f1mpt 5769 isores2 5811 isoini 5816 eloprabga 5959 mpomptx 5963 resoprab 5968 ov6g 6009 dfopab2 6187 dfoprab3s 6188 dfoprab3 6189 f1od2 6233 brtpos2 6249 dftpos3 6260 tpostpos 6262 dfsmo2 6285 elixp2 6699 mapsnen 6808 xpcomco 6823 eqinfti 7016 dfplpq2 7350 dfmpq2 7351 enq0enq 7427 nqnq0a 7450 nqnq0m 7451 genpassl 7520 genpassu 7521 axsuploc 8026 recexre 8531 recexgt0 8533 reapmul1 8548 apsqgt0 8554 apreim 8556 recexaplem2 8605 rerecclap 8683 elznn0 9264 elznn 9265 msqznn 9349 eluz2b1 9597 eluz2b3 9600 qreccl 9638 rpnegap 9682 elfz2nn0 10107 elfzo3 10158 frecuzrdgtcl 10407 frecuzrdgfunlem 10414 qexpclz 10536 shftidt2 10834 clim0 11286 iser3shft 11347 summodclem3 11381 fprod2dlemstep 11623 eftlub 11691 ndvdsadd 11928 algfx 12044 isprm3 12110 isprm5 12134 isabl2 13028 dvdsrcl2 13199 unitinvcl 13223 unitinvinv 13224 unitlinv 13226 unitrinv 13227 ssntr 13493 tx1cn 13640 tx2cn 13641 pilem1 14071 lgsdir2lem4 14303 |
Copyright terms: Public domain | W3C validator |