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  832  oranabs  998  pm5.61  999  pm5.75  1027  eu6lem  2567  2eu5  2651  ceqsralt  3506  ceqsrexbv  3643  reuind  3748  rabsn  4724  preqsn  4861  dfiun2g  5032  reusv2lem4  5398  reusv2lem5  5399  dfid2  5575  elidinxp  6041  dfoprab2  7463  fsplit  8099  xpsnen  9051  elfpw  9350  rankuni  9854  prprrab  14430  isprm2  16615  ismnd  18624  dfgrp2e  18844  pjfval2  21255  neipeltop  22624  cmpfi  22903  isxms2  23945  ishl2  24878  wwlksn0s  29104  clwwlkn1  29283  clwwlkn2  29286  pjimai  31416  bj-snglc  35838  bj-dfid2ALT  35934  bj-epelb  35938  bj-elid6  36039  isbndx  36638  bianim  37084  inecmo2  37213  inecmo3  37218  dfrefrel2  37373  dfcnvrefrel2  37388  dfsymrel2  37407  dfsymrel4  37409  dfsymrel5  37410  refsymrels2  37423  refsymrel2  37425  refsymrel3  37426  dftrrel2  37435  elfunsALTV2  37551  elfunsALTV3  37552  elfunsALTV4  37553  elfunsALTV5  37554  eldisjs2  37581  cdlemefrs29pre00  39254  cdlemefrs29cpre1  39257  dihglb2  40201  elnonrel  42321  pm13.193  43155