Theorem pm5.32ri 579

Description: Distribution of implication over biconditional (inference form). (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 578	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))
3		ancom 464	. 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓))
4		ancom 464	. 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒))
5	2, 3, 4	3bitr4i 306	1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi1i  627  pm5.36  834  oranabs  1000  pm5.61  1001  pm5.75  1029  eu6lem  2572  2eu5  2656  ceqsralt  3429  ceqsrexbv  3554  reuind  3655  rabsn  4623  preqsn  4758  reusv2lem4  5279  reusv2lem5  5280  elidinxp  5896  dfoprab2  7247  fsplit  7863  fsplitOLD  7864  xpsnen  8707  elfpw  8956  rankuni  9444  prprrab  14004  isprm2  16202  ismnd  18130  dfgrp2e  18347  pjfval2  20625  neipeltop  21980  cmpfi  22259  isxms2  23300  ishl2  24221  wwlksn0s  27899  clwwlkn1  28078  clwwlkn2  28081  pjimai  30211  bj-snglc  34845  bj-epelb  34925  bj-elid6  35025  isbndx  35626  inecmo2  36174  inecmo3  36179  dfrefrel2  36319  dfcnvrefrel2  36332  dfsymrel2  36349  dfsymrel4  36351  dfsymrel5  36352  refsymrels2  36365  refsymrel2  36367  refsymrel3  36368  dftrrel2  36377  elfunsALTV2  36490  elfunsALTV3  36491  elfunsALTV4  36492  elfunsALTV5  36493  eldisjs2  36520  cdlemefrs29pre00  38095  cdlemefrs29cpre1  38098  dihglb2  39042  elnonrel  40810  pm13.193  41643