New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 617 | . 2 | |
3 | 1, 2 | mpbi 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: pm5.32ri 619 biadan2 623 anbi2i 675 abai 770 anabs5 784 pm5.33 848 2eu8 2291 eq2tri 2412 rexbiia 2647 reubiia 2796 rmobiia 2801 rabbiia 2849 ceqsrexbv 2973 euxfr 3022 2reu5 3044 eldif 3221 dfpss3 3355 elimif 3691 eldifsn 3839 elrint 3967 elriin 4038 ltfinex 4464 dfevenfin2 4512 dfoddfin2 4513 opeq 4619 setconslem6 4736 rabxp 4814 eliunxp 4821 elres 4995 fncnv 5158 dff1o5 5295 respreima 5410 dff4 5421 dffo3 5422 fsn 5432 fconst3 5457 fconst4 5458 dff13 5471 isores2 5493 isoini 5497 eloprabga 5578 resoprab 5581 fnov 5591 ov6g 5600 mpt2mptx 5708 txpcofun 5803 addcfnex 5824 brpprod 5839 tcfnex 6244 addccan2nclem1 6263 nchoicelem16 6304 nchoicelem18 6306 |
Copyright terms: Public domain | W3C validator |