Theorem pm5.32ri 670

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 669	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))
3		ancom 466	. 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓))
4		ancom 466	. 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒))
5	2, 3, 4	3bitr4i 292	1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anbi1i  731  pm5.61  749  oranabs  901  pm5.36  923  pm5.75  978  2eu5  2557  ceqsralt  3229  ceqsrexbv  3337  reuind  3411  rabsn  4256  preqsn  4393  reusv2lem4  4872  reusv2lem5  4873  dfoprab2  6701  fsplit  7282  xpsnen  8044  elfpw  8268  rankuni  8726  prprrab  13255  isprm2  15395  ismnd  17297  dfgrp2e  17448  pjfval2  20053  neipeltop  20933  cmpfi  21211  isxms2  22253  ishl2  23166  wwlksn0s  26746  clwwlksn2  26910  pjimai  29035  bj-snglc  32957  isbndx  33581  inecmo2  34121  inecmo3  34126  cdlemefrs29pre00  35683  cdlemefrs29cpre1  35686  dihglb2  36631  elnonrel  37891  pm13.193  38612