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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi1i  623  pm5.36  831  oranabs  996  pm5.61  997  pm5.75  1025  eu6lem  2561  2eu5  2645  ceqsralt  3501  ceqsrexbv  3639  reuind  3744  rabsn  4720  preqsn  4857  dfiun2g  5026  reusv2lem4  5392  reusv2lem5  5393  dfid2  5569  elidinxp  6037  dfoprab2  7463  fsplit  8103  xpsnen  9057  elfpw  9356  rankuni  9860  prprrab  14440  isprm2  16626  ismnd  18670  dfgrp2e  18893  pjfval2  21604  neipeltop  22988  cmpfi  23267  isxms2  24309  ishl2  25253  wwlksn0s  29624  clwwlkn1  29803  clwwlkn2  29806  pjimai  31938  bj-snglc  36357  bj-dfid2ALT  36453  bj-epelb  36457  bj-elid6  36558  isbndx  37163  bianim  37609  inecmo2  37738  inecmo3  37743  dfrefrel2  37898  dfcnvrefrel2  37913  dfsymrel2  37932  dfsymrel4  37934  dfsymrel5  37935  refsymrels2  37948  refsymrel2  37950  refsymrel3  37951  dftrrel2  37960  elfunsALTV2  38076  elfunsALTV3  38077  elfunsALTV4  38078  elfunsALTV5  38079  eldisjs2  38106  cdlemefrs29pre00  39779  cdlemefrs29cpre1  39782  dihglb2  40726  elnonrel  42912  pm13.193  43746