Theorem pm5.32ri 580

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  bianim  581  anbi1i  630  pm5.36  839  oranabs  1007  pm5.61  1008  pm5.75  1036  eu6lem  2577  2eu5  2660  ceqsralt  3467  ceqsrexbv  3601  reuind  3701  rabsn  4660  preqsn  4800  dfiun2g  4966  reusv2lem4  5337  reusv2lem5  5338  dfid2  5522  elidinxp  6003  dfoprab2  7421  fsplit  8063  xpsnen  8996  elfpw  9261  rankuni  9785  prprrab  14433  isprm2  16649  ismnd  18703  dfgrp2e  18937  pjfval2  21691  neipeltop  23119  cmpfi  23398  isxms2  24438  ishl2  25362  wwlksn0s  29954  clwwlkn1  30136  clwwlkn2  30139  pjimai  32272  bj-snglc  37329  bj-dfid2ALT  37425  bj-epelb  37429  bj-elid6  37537  isbndx  38156  inecmo2  38730  inecmo3  38743  dfrefrel2  38969  dfcnvrefrel2  38984  dfsymrel2  39007  dfsymrel4  39009  dfsymrel5  39010  refsymrels2  39023  refsymrel2  39025  refsymrel3  39026  dftrrel2  39035  elfunsALTV2  39152  elfunsALTV3  39153  elfunsALTV4  39154  elfunsALTV5  39155  eldisjs2  39194  cdlemefrs29pre00  40894  cdlemefrs29cpre1  40897  dihglb2  41841  redvmptabs  42844  elnonrel  44036  pm13.193  44862  dfnbgr6  48355