Theorem pm5.32ri 585

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

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

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 401

This theorem is referenced by:  bianim  586  anbi1i  635  pm5.36  846  oranabs  1015  pm5.61  1016  pm5.75  1046  eu6lem  2601  2eu5  2683  ceqsralt  3489  ceqsrexbv  3616  reuind  3717  rabsn  4688  preqsn  4828  dfiun2g  4995  reusv2lem4  5374  reusv2lem5  5375  dfid2  5560  elidinxp  6048  dfoprab2  7470  fsplit  8113  xpsnen  9050  elfpw  9312  rankuni  9836  prprrab  14512  isprm2  16741  ismnd  18796  dfgrp2e  19031  pjfval2  21840  neipeltop  23267  cmpfi  23546  isxms2  24586  ishl2  25510  wwlksn0s  30191  clwwlkn1  30373  clwwlkn2  30376  pjimai  32509  bj-snglc  37586  bj-dfid2ALT  37682  bj-epelb  37686  bj-elid6  37795  isbndx  38414  inecmo2  38986  inecmo3  38999  dfrefrel2  39225  dfcnvrefrel2  39240  dfsymrel2  39263  dfsymrel4  39265  dfsymrel5  39266  refsymrels2  39279  refsymrel2  39281  refsymrel3  39282  dftrrel2  39291  elfunsALTV2  39408  elfunsALTV3  39409  elfunsALTV4  39410  elfunsALTV5  39411  eldisjs2  39450  cdlemefrs29pre00  41150  cdlemefrs29cpre1  41153  dihglb2  42097  redvmptabs  43102  elnonrel  44294  pm13.193  45104  dfnbgr6  48605  2alsraln0  50578