![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm5.32i | GIF 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: → wi 4 ∧ wa 104 ↔ wb 105 |
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 3957 opeqsn 4252 rabxp 4663 eliunxp 4766 restidsing 4963 ressn 5169 fncnv 5282 dff1o5 5470 respreima 5644 dff4im 5662 dffo3 5663 f1ompt 5667 fsn 5688 fconst3m 5735 fconst4m 5736 eufnfv 5747 dff13 5768 f1mpt 5771 isores2 5813 isoini 5818 eloprabga 5961 mpomptx 5965 resoprab 5970 ov6g 6011 dfopab2 6189 dfoprab3s 6190 dfoprab3 6191 f1od2 6235 brtpos2 6251 dftpos3 6262 tpostpos 6264 dfsmo2 6287 elixp2 6701 mapsnen 6810 xpcomco 6825 eqinfti 7018 dfplpq2 7352 dfmpq2 7353 enq0enq 7429 nqnq0a 7452 nqnq0m 7453 genpassl 7522 genpassu 7523 axsuploc 8029 recexre 8534 recexgt0 8536 reapmul1 8551 apsqgt0 8557 apreim 8559 recexaplem2 8608 rerecclap 8686 elznn0 9267 elznn 9268 msqznn 9352 eluz2b1 9600 eluz2b3 9603 qreccl 9641 rpnegap 9685 elfz2nn0 10111 elfzo3 10162 frecuzrdgtcl 10411 frecuzrdgfunlem 10418 qexpclz 10540 shftidt2 10840 clim0 11292 iser3shft 11353 summodclem3 11387 fprod2dlemstep 11629 eftlub 11697 ndvdsadd 11935 algfx 12051 isprm3 12117 isprm5 12141 xpsfrnel 12762 isabl2 13095 dvdsrcl2 13266 unitinvcl 13290 unitinvinv 13291 unitlinv 13293 unitrinv 13294 ssntr 13558 tx1cn 13705 tx2cn 13706 pilem1 14136 lgsdir2lem4 14368 |
Copyright terms: Public domain | W3C validator |