Theorem pm5.32ri 575

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bianim  576  anbi1i  624  pm5.36  833  oranabs  1001  pm5.61  1002  pm5.75  1030  eu6lem  2567  2eu5  2650  ceqsralt  3485  ceqsrexbv  3625  reuind  3727  rabsn  4688  preqsn  4829  dfiun2g  4997  reusv2lem4  5359  reusv2lem5  5360  dfid2  5538  elidinxp  6018  dfoprab2  7450  fsplit  8099  xpsnen  9029  elfpw  9312  rankuni  9823  prprrab  14445  isprm2  16659  ismnd  18671  dfgrp2e  18902  pjfval2  21625  neipeltop  23023  cmpfi  23302  isxms2  24343  ishl2  25277  wwlksn0s  29798  clwwlkn1  29977  clwwlkn2  29980  pjimai  32112  bj-snglc  36964  bj-dfid2ALT  37060  bj-epelb  37064  bj-elid6  37165  isbndx  37783  inecmo2  38345  inecmo3  38350  dfrefrel2  38513  dfcnvrefrel2  38528  dfsymrel2  38547  dfsymrel4  38549  dfsymrel5  38550  refsymrels2  38563  refsymrel2  38565  refsymrel3  38566  dftrrel2  38575  elfunsALTV2  38692  elfunsALTV3  38693  elfunsALTV4  38694  elfunsALTV5  38695  eldisjs2  38722  cdlemefrs29pre00  40396  cdlemefrs29cpre1  40399  dihglb2  41343  redvmptabs  42355  elnonrel  43581  pm13.193  44407  dfnbgr6  47861