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  834  oranabs  1001  pm5.61  1002  pm5.75  1030  eu6lem  2570  2eu5  2653  ceqsralt  3513  ceqsrexbv  3655  reuind  3761  rabsn  4725  preqsn  4866  dfiun2g  5034  reusv2lem4  5406  reusv2lem5  5407  dfid2  5584  elidinxp  6063  dfoprab2  7490  fsplit  8140  xpsnen  9093  elfpw  9391  rankuni  9900  prprrab  14508  isprm2  16715  ismnd  18762  dfgrp2e  18993  pjfval2  21746  neipeltop  23152  cmpfi  23431  isxms2  24473  ishl2  25417  wwlksn0s  29890  clwwlkn1  30069  clwwlkn2  30072  pjimai  32204  bj-snglc  36951  bj-dfid2ALT  37047  bj-epelb  37051  bj-elid6  37152  isbndx  37768  inecmo2  38337  inecmo3  38342  dfrefrel2  38496  dfcnvrefrel2  38511  dfsymrel2  38530  dfsymrel4  38532  dfsymrel5  38533  refsymrels2  38546  refsymrel2  38548  refsymrel3  38549  dftrrel2  38558  elfunsALTV2  38674  elfunsALTV3  38675  elfunsALTV4  38676  elfunsALTV5  38677  eldisjs2  38704  cdlemefrs29pre00  40377  cdlemefrs29cpre1  40380  dihglb2  41324  redvmptabs  42368  elnonrel  43574  pm13.193  44406  dfnbgr6  47780