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

This theorem is referenced by:  bianim  576  anbi1i  624  pm5.36  833  oranabs  1001  pm5.61  1002  pm5.75  1030  eu6lem  2566  2eu5  2649  ceqsralt  3482  ceqsrexbv  3622  reuind  3724  rabsn  4685  preqsn  4826  dfiun2g  4994  reusv2lem4  5356  reusv2lem5  5357  dfid2  5535  elidinxp  6015  dfoprab2  7447  fsplit  8096  xpsnen  9025  elfpw  9305  rankuni  9816  prprrab  14438  isprm2  16652  ismnd  18664  dfgrp2e  18895  pjfval2  21618  neipeltop  23016  cmpfi  23295  isxms2  24336  ishl2  25270  wwlksn0s  29791  clwwlkn1  29970  clwwlkn2  29973  pjimai  32105  bj-snglc  36957  bj-dfid2ALT  37053  bj-epelb  37057  bj-elid6  37158  isbndx  37776  inecmo2  38338  inecmo3  38343  dfrefrel2  38506  dfcnvrefrel2  38521  dfsymrel2  38540  dfsymrel4  38542  dfsymrel5  38543  refsymrels2  38556  refsymrel2  38558  refsymrel3  38559  dftrrel2  38568  elfunsALTV2  38685  elfunsALTV3  38686  elfunsALTV4  38687  elfunsALTV5  38688  eldisjs2  38715  cdlemefrs29pre00  40389  cdlemefrs29cpre1  40392  dihglb2  41336  redvmptabs  42348  elnonrel  43574  pm13.193  44400  dfnbgr6  47857