![]() |
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 567 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
3 | ancom 453 | . 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | |
4 | ancom 453 | . 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4i 295 | 1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: anbi1i 615 pm5.36 822 oranabs 983 pm5.61 984 pm5.75 1012 eu6lem 2590 eu6OLDOLD 2594 2eu5 2689 ceqsralt 3444 ceqsrexbv 3559 reuind 3648 rabsn 4528 preqsn 4663 reusv2lem4 5152 reusv2lem5 5153 elidinxp 5754 dfoprab2 7030 fsplit 7619 xpsnen 8396 elfpw 8620 rankuni 9085 prprrab 13641 isprm2 15881 ismnd 17778 dfgrp2e 17930 pjfval2 20571 neipeltop 21457 cmpfi 21736 isxms2 22777 ishl2 23692 wwlksn0s 27363 clwwlkn1 27573 clwwlkn2 27576 pjimai 29750 bj-snglc 33832 isbndx 34535 inecmo2 35089 inecmo3 35094 dfrefrel2 35233 dfcnvrefrel2 35246 dfsymrel2 35263 dfsymrel4 35265 dfsymrel5 35266 refsymrels2 35279 refsymrel2 35281 refsymrel3 35282 dftrrel2 35291 elfunsALTV2 35404 elfunsALTV3 35405 elfunsALTV4 35406 elfunsALTV5 35407 eldisjs2 35434 cdlemefrs29pre00 37009 cdlemefrs29cpre1 37012 dihglb2 37956 elnonrel 39341 pm13.193 40194 |
Copyright terms: Public domain | W3C validator |