Theorem pm5.32ri 583

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bianim  584  anbi1i  633  pm5.36  844  oranabs  1012  pm5.61  1013  pm5.75  1041  eu6lem  2599  2eu5  2681  ceqsralt  3487  ceqsrexbv  3615  reuind  3715  rabsn  4679  preqsn  4819  dfiun2g  4986  reusv2lem4  5357  reusv2lem5  5358  dfid2  5542  elidinxp  6030  dfoprab2  7450  fsplit  8091  xpsnen  9029  elfpw  9294  rankuni  9818  prprrab  14483  isprm2  16699  ismnd  18754  dfgrp2e  18988  pjfval2  21741  neipeltop  23169  cmpfi  23448  isxms2  24488  ishl2  25412  wwlksn0s  30007  clwwlkn1  30189  clwwlkn2  30192  pjimai  32325  bj-snglc  37418  bj-dfid2ALT  37514  bj-epelb  37518  bj-elid6  37626  isbndx  38245  inecmo2  38819  inecmo3  38832  dfrefrel2  39058  dfcnvrefrel2  39073  dfsymrel2  39096  dfsymrel4  39098  dfsymrel5  39099  refsymrels2  39112  refsymrel2  39114  refsymrel3  39115  dftrrel2  39124  elfunsALTV2  39241  elfunsALTV3  39242  elfunsALTV4  39243  elfunsALTV5  39244  eldisjs2  39283  cdlemefrs29pre00  40983  cdlemefrs29cpre1  40986  dihglb2  41930  redvmptabs  42933  elnonrel  44125  pm13.193  44951  dfnbgr6  48443