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  2601  2eu5  2683  ceqsralt  3488  ceqsrexbv  3613  reuind  3714  rabsn  4682  preqsn  4820  dfiun2g  4991  reusv2lem4  5368  reusv2lem5  5369  dfid2  5553  elidinxp  6049  dfoprab2  7504  fsplit  8158  xpsnen  9111  elfpw  9374  rankuni  9909  prprrab  14648  isprm2  16889  ismnd  18958  dfgrp2e  19206  pjfval2  22048  neipeltop  23480  cmpfi  23759  isxms2  24800  ishl2  25724  wwlksn0s  30483  clwwlkn1  30665  clwwlkn2  30668  pjimai  32811  bj-snglc  38073  bj-elinxp  38151  bj-dfid2ALT  38184  bj-epelb  38188  bj-elid6  38296  isbndx  38919  inecmo2  39491  inecmo3  39504  dfrefrel2  39730  dfcnvrefrel2  39745  dfsymrel2  39768  dfsymrel4  39770  dfsymrel5  39771  refsymrels2  39784  refsymrel2  39786  refsymrel3  39787  dftrrel2  39796  elfunsALTV2  39913  elfunsALTV3  39914  elfunsALTV4  39915  elfunsALTV5  39916  eldisjs2  39955  cdlemefrs29pre00  41655  cdlemefrs29cpre1  41658  dihglb2  42602  redvmptabs  43615  elnonrel  44789  pm13.193  45598  dfnbgr6  49170  2alsraln0  51225