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  834  oranabs  1002  pm5.61  1003  pm5.75  1031  eu6lem  2573  2eu5  2656  ceqsralt  3516  ceqsrexbv  3656  reuind  3759  rabsn  4721  preqsn  4862  dfiun2g  5030  reusv2lem4  5401  reusv2lem5  5402  dfid2  5580  elidinxp  6062  dfoprab2  7491  fsplit  8142  xpsnen  9095  elfpw  9394  rankuni  9903  prprrab  14512  isprm2  16719  ismnd  18750  dfgrp2e  18981  pjfval2  21729  neipeltop  23137  cmpfi  23416  isxms2  24458  ishl2  25404  wwlksn0s  29881  clwwlkn1  30060  clwwlkn2  30063  pjimai  32195  bj-snglc  36970  bj-dfid2ALT  37066  bj-epelb  37070  bj-elid6  37171  isbndx  37789  inecmo2  38357  inecmo3  38362  dfrefrel2  38516  dfcnvrefrel2  38531  dfsymrel2  38550  dfsymrel4  38552  dfsymrel5  38553  refsymrels2  38566  refsymrel2  38568  refsymrel3  38569  dftrrel2  38578  elfunsALTV2  38694  elfunsALTV3  38695  elfunsALTV4  38696  elfunsALTV5  38697  eldisjs2  38724  cdlemefrs29pre00  40397  cdlemefrs29cpre1  40400  dihglb2  41344  redvmptabs  42390  elnonrel  43598  pm13.193  44430  dfnbgr6  47843