Theorem pm5.32ri 586

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianim  587  anbi1i  636  pm5.36  847  oranabs  1015  pm5.61  1016  pm5.75  1046  eu6lem  2598  2eu5  2680  ceqsralt  3484  ceqsrexbv  3609  reuind  3710  rabsn  4678  preqsn  4816  dfiun2g  4987  reusv2lem4  5362  reusv2lem5  5363  dfid2  5547  elidinxp  6035  dfoprab2  7478  fsplit  8130  xpsnen  9083  elfpw  9346  rankuni  9882  prprrab  14621  isprm2  16862  ismnd  18931  dfgrp2e  19179  pjfval2  22020  neipeltop  23452  cmpfi  23731  isxms2  24772  ishl2  25696  wwlksn0s  30455  clwwlkn1  30637  clwwlkn2  30640  pjimai  32783  bj-snglc  37974  bj-dfid2ALT  38072  bj-epelb  38076  bj-elid6  38184  isbndx  38809  inecmo2  39381  inecmo3  39394  dfrefrel2  39620  dfcnvrefrel2  39635  dfsymrel2  39658  dfsymrel4  39660  dfsymrel5  39661  refsymrels2  39674  refsymrel2  39676  refsymrel3  39677  dftrrel2  39686  elfunsALTV2  39803  elfunsALTV3  39804  elfunsALTV4  39805  elfunsALTV5  39806  eldisjs2  39845  cdlemefrs29pre00  41545  cdlemefrs29cpre1  41548  dihglb2  42492  redvmptabs  43504  elnonrel  44679  pm13.193  45488  dfnbgr6  49048  2alsraln0  51081