Theorem pm5.32ri 568

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  anbi1i  615  pm5.36  822  oranabs  983  pm5.61  984  pm5.75  1012  eu6lem  2590  eu6OLDOLD  2594  2eu5  2689  ceqsralt  3444  ceqsrexbv  3559  reuind  3648  rabsn  4528  preqsn  4663  reusv2lem4  5152  reusv2lem5  5153  elidinxp  5754  dfoprab2  7030  fsplit  7619  xpsnen  8396  elfpw  8620  rankuni  9085  prprrab  13641  isprm2  15881  ismnd  17778  dfgrp2e  17930  pjfval2  20571  neipeltop  21457  cmpfi  21736  isxms2  22777  ishl2  23692  wwlksn0s  27363  clwwlkn1  27573  clwwlkn2  27576  pjimai  29750  bj-snglc  33832  isbndx  34535  inecmo2  35089  inecmo3  35094  dfrefrel2  35233  dfcnvrefrel2  35246  dfsymrel2  35263  dfsymrel4  35265  dfsymrel5  35266  refsymrels2  35279  refsymrel2  35281  refsymrel3  35282  dftrrel2  35291  elfunsALTV2  35404  elfunsALTV3  35405  elfunsALTV4  35406  elfunsALTV5  35407  eldisjs2  35434  cdlemefrs29pre00  37009  cdlemefrs29cpre1  37012  dihglb2  37956  elnonrel  39341  pm13.193  40194