Theorem pm5.32ri 578

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anbi1i  625  pm5.36  831  oranabs  996  pm5.61  997  pm5.75  1025  eu6lem  2658  2eu5  2740  2eu5OLD  2741  ceqsralt  3528  ceqsrexbv  3650  reuind  3744  rabsn  4657  preqsn  4792  reusv2lem4  5302  reusv2lem5  5303  elidinxp  5911  dfoprab2  7212  fsplit  7812  fsplitOLD  7813  xpsnen  8601  elfpw  8826  rankuni  9292  prprrab  13832  isprm2  16026  ismnd  17914  dfgrp2e  18129  pjfval2  20853  neipeltop  21737  cmpfi  22016  isxms2  23058  ishl2  23973  wwlksn0s  27639  clwwlkn1  27819  clwwlkn2  27822  pjimai  29953  bj-snglc  34284  bj-epelb  34364  bj-elid6  34465  isbndx  35075  inecmo2  35625  inecmo3  35630  dfrefrel2  35770  dfcnvrefrel2  35783  dfsymrel2  35800  dfsymrel4  35802  dfsymrel5  35803  refsymrels2  35816  refsymrel2  35818  refsymrel3  35819  dftrrel2  35828  elfunsALTV2  35941  elfunsALTV3  35942  elfunsALTV4  35943  elfunsALTV5  35944  eldisjs2  35971  cdlemefrs29pre00  37546  cdlemefrs29cpre1  37549  dihglb2  38493  elnonrel  39965  pm13.193  40763