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 449 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.32ri 451 biadan2 452 anbi2i 453 abai 550 anabs5 563 pm5.33 599 eq2tri 2200 rexbiia 2453 reubiia 2618 rmobiia 2623 rabbiia 2674 ceqsrexbv 2820 euxfrdc 2874 eldifpr 3559 eldiftp 3577 eldifsn 3658 elrint 3819 elriin 3891 opeqsn 4182 rabxp 4584 eliunxp 4686 ressn 5087 fncnv 5197 dff1o5 5384 respreima 5556 dff4im 5574 dffo3 5575 f1ompt 5579 fsn 5600 fconst3m 5647 fconst4m 5648 eufnfv 5656 dff13 5677 f1mpt 5680 isores2 5722 isoini 5727 eloprabga 5866 mpomptx 5870 resoprab 5875 ov6g 5916 dfopab2 6095 dfoprab3s 6096 dfoprab3 6097 f1od2 6140 brtpos2 6156 dftpos3 6167 tpostpos 6169 dfsmo2 6192 elixp2 6604 mapsnen 6713 xpcomco 6728 eqinfti 6915 dfplpq2 7186 dfmpq2 7187 enq0enq 7263 nqnq0a 7286 nqnq0m 7287 genpassl 7356 genpassu 7357 axsuploc 7861 recexre 8364 recexgt0 8366 reapmul1 8381 apsqgt0 8387 apreim 8389 recexaplem2 8437 rerecclap 8514 elznn0 9093 elznn 9094 msqznn 9175 eluz2b1 9422 eluz2b3 9425 qreccl 9461 rpnegap 9503 elfz2nn0 9923 elfzo3 9971 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 qexpclz 10345 shftidt2 10636 clim0 11086 iser3shft 11147 summodclem3 11181 eftlub 11433 ndvdsadd 11664 algfx 11769 isprm3 11835 ssntr 12330 tx1cn 12477 tx2cn 12478 pilem1 12908 |
Copyright terms: Public domain | W3C validator |