![]() |
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 574 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
3 | ancom 460 | . 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | |
4 | ancom 460 | . 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 |
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 206 df-an 396 |
This theorem is referenced by: anbi1i 623 pm5.36 831 oranabs 996 pm5.61 997 pm5.75 1025 eu6lem 2561 2eu5 2645 ceqsralt 3501 ceqsrexbv 3639 reuind 3744 rabsn 4720 preqsn 4857 dfiun2g 5026 reusv2lem4 5392 reusv2lem5 5393 dfid2 5569 elidinxp 6037 dfoprab2 7463 fsplit 8103 xpsnen 9057 elfpw 9356 rankuni 9860 prprrab 14440 isprm2 16626 ismnd 18670 dfgrp2e 18893 pjfval2 21604 neipeltop 22988 cmpfi 23267 isxms2 24309 ishl2 25253 wwlksn0s 29624 clwwlkn1 29803 clwwlkn2 29806 pjimai 31938 bj-snglc 36357 bj-dfid2ALT 36453 bj-epelb 36457 bj-elid6 36558 isbndx 37163 bianim 37609 inecmo2 37738 inecmo3 37743 dfrefrel2 37898 dfcnvrefrel2 37913 dfsymrel2 37932 dfsymrel4 37934 dfsymrel5 37935 refsymrels2 37948 refsymrel2 37950 refsymrel3 37951 dftrrel2 37960 elfunsALTV2 38076 elfunsALTV3 38077 elfunsALTV4 38078 elfunsALTV5 38079 eldisjs2 38106 cdlemefrs29pre00 39779 cdlemefrs29cpre1 39782 dihglb2 40726 elnonrel 42912 pm13.193 43746 |
Copyright terms: Public domain | W3C validator |