Theorem pm5.32ri 585

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bianim  586  anbi1i  635  pm5.36  846  oranabs  1015  pm5.61  1016  pm5.75  1044  eu6lem  2607  2eu5  2689  ceqsralt  3497  ceqsrexbv  3624  reuind  3725  rabsn  4689  preqsn  4828  dfiun2g  4995  reusv2lem4  5370  reusv2lem5  5371  dfid2  5556  elidinxp  6044  dfoprab2  7466  fsplit  8108  xpsnen  9045  elfpw  9307  rankuni  9831  prprrab  14506  isprm2  16736  ismnd  18791  dfgrp2e  19026  pjfval2  21824  neipeltop  23251  cmpfi  23530  isxms2  24570  ishl2  25494  wwlksn0s  30147  clwwlkn1  30329  clwwlkn2  30332  pjimai  32465  bj-snglc  37489  bj-dfid2ALT  37585  bj-epelb  37589  bj-elid6  37697  isbndx  38316  inecmo2  38890  inecmo3  38903  dfrefrel2  39129  dfcnvrefrel2  39144  dfsymrel2  39167  dfsymrel4  39169  dfsymrel5  39170  refsymrels2  39183  refsymrel2  39185  refsymrel3  39186  dftrrel2  39195  elfunsALTV2  39312  elfunsALTV3  39313  elfunsALTV4  39314  elfunsALTV5  39315  eldisjs2  39354  cdlemefrs29pre00  41054  cdlemefrs29cpre1  41057  dihglb2  42001  redvmptabs  43004  elnonrel  44196  pm13.193  45006  dfnbgr6  48504