Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.32ri | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
pm5.32i.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.32ri | ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32i.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.32i 667 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
3 | ancom 465 | . 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | |
4 | ancom 465 | . 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4i 291 | 1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: anbi1i 727 pm5.61 745 oranabs 897 pm5.36 919 pm5.75 974 2eu5 2545 ceqsralt 3202 ceqsrexbv 3307 reuind 3378 rabsn 4200 preqsn 4331 reusv2lem4 4798 reusv2lem5 4799 dfoprab2 6599 fsplit 7169 xpsnen 7929 elfpw 8151 rankuni 8609 prprrab 13112 isprm2 15233 ismnd 17120 dfgrp2e 17271 pjfval2 19872 neipeltop 20743 cmpfi 21021 isxms2 22063 ishl2 22974 usgraop 25879 pjimai 28419 bj-snglc 32150 isbndx 32751 cdlemefrs29pre00 34701 cdlemefrs29cpre1 34704 dihglb2 35649 elnonrel 36910 pm13.193 37634 wwlksn0s 41057 clwwlksn2 41217 |
Copyright terms: Public domain | W3C validator |