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 form). (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 575 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
3 | ancom 461 | . 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | |
4 | ancom 461 | . 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: anbi1i 623 pm5.36 829 oranabs 993 pm5.61 994 pm5.75 1022 eu6lem 2651 2eu5 2735 2eu5OLD 2736 ceqsralt 3526 ceqsrexbv 3647 reuind 3741 rabsn 4649 preqsn 4784 reusv2lem4 5292 reusv2lem5 5293 elidinxp 5904 dfoprab2 7201 fsplit 7801 fsplitOLD 7802 xpsnen 8589 elfpw 8814 rankuni 9280 prprrab 13819 isprm2 16014 ismnd 17902 dfgrp2e 18067 pjfval2 20781 neipeltop 21665 cmpfi 21944 isxms2 22985 ishl2 23900 wwlksn0s 27566 clwwlkn1 27746 clwwlkn2 27749 pjimai 29880 bj-snglc 34178 bj-epelb 34255 bj-elid6 34354 isbndx 34941 inecmo2 35491 inecmo3 35496 dfrefrel2 35635 dfcnvrefrel2 35648 dfsymrel2 35665 dfsymrel4 35667 dfsymrel5 35668 refsymrels2 35681 refsymrel2 35683 refsymrel3 35684 dftrrel2 35693 elfunsALTV2 35806 elfunsALTV3 35807 elfunsALTV4 35808 elfunsALTV5 35809 eldisjs2 35836 cdlemefrs29pre00 37411 cdlemefrs29cpre1 37414 dihglb2 38358 elnonrel 39823 pm13.193 40620 |
Copyright terms: Public domain | W3C validator |