Theorem pm5.32ri 576

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anbi1i  624  pm5.36  831  oranabs  997  pm5.61  998  pm5.75  1026  eu6lem  2572  2eu5  2656  ceqsralt  3472  ceqsrexbv  3595  reuind  3697  rabsn  4665  preqsn  4802  dfiun2g  4971  reusv2lem4  5337  reusv2lem5  5338  dfid2  5507  elidinxp  5968  dfoprab2  7371  fsplit  8000  xpsnen  8895  elfpw  9189  rankuni  9689  prprrab  14256  isprm2  16454  ismnd  18455  dfgrp2e  18672  pjfval2  20987  neipeltop  22351  cmpfi  22630  isxms2  23672  ishl2  24605  wwlksn0s  28334  clwwlkn1  28513  clwwlkn2  28516  pjimai  30646  bj-snglc  35219  bj-dfid2ALT  35296  bj-epelb  35300  bj-elid6  35401  isbndx  36000  bianim  36447  inecmo2  36581  inecmo3  36586  dfrefrel2  36741  dfcnvrefrel2  36756  dfsymrel2  36775  dfsymrel4  36777  dfsymrel5  36778  refsymrels2  36791  refsymrel2  36793  refsymrel3  36794  dftrrel2  36803  elfunsALTV2  36919  elfunsALTV3  36920  elfunsALTV4  36921  elfunsALTV5  36922  eldisjs2  36949  cdlemefrs29pre00  38621  cdlemefrs29cpre1  38624  dihglb2  39568  elnonrel  41421  pm13.193  42257