Theorem pm5.32ri 668

Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)

Hypothesis

Ref	Expression
pm5.32i.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
pm5.32ri	⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

Proof of Theorem 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 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

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