Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.32i | Unicode version |
Description: Distribution of implication over biconditional (inference rule). (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 426 | . 2 | |
3 | 1, 2 | mpbi 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.32ri 428 biadan2 429 anbi2i 430 abai 494 anabs5 507 pm5.33 541 eq2tri 2099 rexbiia 2339 reubiia 2494 rmobiia 2499 rabbiia 2547 ceqsrexbv 2675 euxfrdc 2727 dfpss3 3030 eldifsn 3495 elrint 3655 elriin 3727 opeqsn 3989 rabxp 4380 eliunxp 4475 ressn 4858 fncnv 4965 dff1o5 5135 respreima 5295 dff4im 5313 dffo3 5314 f1ompt 5320 fsn 5335 fconst3m 5380 fconst4m 5381 eufnfv 5389 dff13 5407 f1mpt 5410 isores2 5453 isoini 5457 eloprabga 5591 mpt2mptx 5595 resoprab 5597 ov6g 5638 dfopab2 5815 dfoprab3s 5816 dfoprab3 5817 brtpos2 5866 dftpos3 5877 tpostpos 5879 dfsmo2 5902 xpcomco 6300 dfplpq2 6452 dfmpq2 6453 enq0enq 6529 nqnq0a 6552 nqnq0m 6553 genpassl 6622 genpassu 6623 recexre 7569 recexgt0 7571 reapmul1 7586 apsqgt0 7592 apreim 7594 recexaplem2 7633 rerecclap 7706 elznn0 8260 elznn 8261 msqznn 8338 eluz2b1 8539 eluz2b3 8541 qreccl 8576 rpnegap 8615 elfz2nn0 8973 elfzo3 9019 frecuzrdgfn 9198 qexpclz 9276 shftidt2 9433 clim0 9806 ialgfx 9891 |
Copyright terms: Public domain | W3C validator |