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  625  pm5.36  834  oranabs  1002  pm5.61  1003  pm5.75  1031  eu6lem  2574  2eu5  2657  ceqsralt  3477  ceqsrexbv  3612  reuind  3713  rabsn  4680  preqsn  4820  dfiun2g  4987  reusv2lem4  5348  reusv2lem5  5349  dfid2  5529  elidinxp  6011  dfoprab2  7426  fsplit  8069  xpsnen  9001  elfpw  9266  rankuni  9787  prprrab  14408  isprm2  16621  ismnd  18674  dfgrp2e  18905  pjfval2  21676  neipeltop  23085  cmpfi  23364  isxms2  24404  ishl2  25338  wwlksn0s  29946  clwwlkn1  30128  clwwlkn2  30131  pjimai  32263  bj-snglc  37214  bj-dfid2ALT  37310  bj-epelb  37314  bj-elid6  37422  isbndx  38030  inecmo2  38604  inecmo3  38617  dfrefrel2  38843  dfcnvrefrel2  38858  dfsymrel2  38881  dfsymrel4  38883  dfsymrel5  38884  refsymrels2  38897  refsymrel2  38899  refsymrel3  38900  dftrrel2  38909  elfunsALTV2  39026  elfunsALTV3  39027  elfunsALTV4  39028  elfunsALTV5  39029  eldisjs2  39068  cdlemefrs29pre00  40768  cdlemefrs29cpre1  40771  dihglb2  41715  redvmptabs  42727  elnonrel  43938  pm13.193  44764  dfnbgr6  48214