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  2603  2eu5  2685  ceqsralt  3491  ceqsrexbv  3618  reuind  3719  rabsn  4683  preqsn  4822  dfiun2g  4989  reusv2lem4  5362  reusv2lem5  5363  dfid2  5548  elidinxp  6036  dfoprab2  7458  fsplit  8100  xpsnen  9037  elfpw  9299  rankuni  9823  prprrab  14498  isprm2  16728  ismnd  18783  dfgrp2e  19018  pjfval2  21816  neipeltop  23243  cmpfi  23522  isxms2  24562  ishl2  25486  wwlksn0s  30115  clwwlkn1  30297  clwwlkn2  30300  pjimai  32433  bj-snglc  37461  bj-dfid2ALT  37557  bj-epelb  37561  bj-elid6  37669  isbndx  38288  inecmo2  38862  inecmo3  38875  dfrefrel2  39101  dfcnvrefrel2  39116  dfsymrel2  39139  dfsymrel4  39141  dfsymrel5  39142  refsymrels2  39155  refsymrel2  39157  refsymrel3  39158  dftrrel2  39167  elfunsALTV2  39284  elfunsALTV3  39285  elfunsALTV4  39286  elfunsALTV5  39287  eldisjs2  39326  cdlemefrs29pre00  41026  cdlemefrs29cpre1  41029  dihglb2  41973  redvmptabs  42976  elnonrel  44168  pm13.193  44980  dfnbgr6  48478