![]() |
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 2662 rmobiia 2667 rabbiia 2723 ceqsrexbv 2869 euxfrdc 2924 eldifpr 3620 eldiftp 3639 eldifsn 3720 elrint 3885 elriin 3958 opeqsn 4253 rabxp 4664 eliunxp 4767 restidsing 4964 ressn 5170 fncnv 5283 dff1o5 5471 respreima 5645 dff4im 5663 dffo3 5664 f1ompt 5668 fsn 5689 fconst3m 5736 fconst4m 5737 eufnfv 5748 dff13 5769 f1mpt 5772 isores2 5814 isoini 5819 eloprabga 5962 mpomptx 5966 resoprab 5971 ov6g 6012 dfopab2 6190 dfoprab3s 6191 dfoprab3 6192 f1od2 6236 brtpos2 6252 dftpos3 6263 tpostpos 6265 dfsmo2 6288 elixp2 6702 mapsnen 6811 xpcomco 6826 eqinfti 7019 dfplpq2 7353 dfmpq2 7354 enq0enq 7430 nqnq0a 7453 nqnq0m 7454 genpassl 7523 genpassu 7524 axsuploc 8030 recexre 8535 recexgt0 8537 reapmul1 8552 apsqgt0 8558 apreim 8560 recexaplem2 8609 rerecclap 8687 elznn0 9268 elznn 9269 msqznn 9353 eluz2b1 9601 eluz2b3 9604 qreccl 9642 rpnegap 9686 elfz2nn0 10112 elfzo3 10163 frecuzrdgtcl 10412 frecuzrdgfunlem 10419 qexpclz 10541 shftidt2 10841 clim0 11293 iser3shft 11354 summodclem3 11388 fprod2dlemstep 11630 eftlub 11698 ndvdsadd 11936 algfx 12052 isprm3 12118 isprm5 12142 xpsfrnel 12763 isabl2 13097 dvdsrcl2 13268 unitinvcl 13292 unitinvinv 13293 unitlinv 13295 unitrinv 13296 islmod 13381 ssntr 13625 tx1cn 13772 tx2cn 13773 pilem1 14203 lgsdir2lem4 14435 |
Copyright terms: Public domain | W3C validator |