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  2566  2eu5  2649  ceqsralt  3473  ceqsrexbv  3613  reuind  3715  rabsn  4675  preqsn  4816  dfiun2g  4983  reusv2lem4  5343  reusv2lem5  5344  dfid2  5520  elidinxp  5999  dfoprab2  7411  fsplit  8057  xpsnen  8985  elfpw  9263  rankuni  9778  prprrab  14398  isprm2  16611  ismnd  18629  dfgrp2e  18860  pjfval2  21634  neipeltop  23032  cmpfi  23311  isxms2  24352  ishl2  25286  wwlksn0s  29824  clwwlkn1  30003  clwwlkn2  30006  pjimai  32138  bj-snglc  36942  bj-dfid2ALT  37038  bj-epelb  37042  bj-elid6  37143  isbndx  37761  inecmo2  38323  inecmo3  38328  dfrefrel2  38491  dfcnvrefrel2  38506  dfsymrel2  38525  dfsymrel4  38527  dfsymrel5  38528  refsymrels2  38541  refsymrel2  38543  refsymrel3  38544  dftrrel2  38553  elfunsALTV2  38670  elfunsALTV3  38671  elfunsALTV4  38672  elfunsALTV5  38673  eldisjs2  38700  cdlemefrs29pre00  40374  cdlemefrs29cpre1  40377  dihglb2  41321  redvmptabs  42333  elnonrel  43558  pm13.193  44384  dfnbgr6  47842