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  2568  2eu5  2651  ceqsralt  3471  ceqsrexbv  3611  reuind  3712  rabsn  4674  preqsn  4814  dfiun2g  4980  reusv2lem4  5339  reusv2lem5  5340  dfid2  5513  elidinxp  5993  dfoprab2  7404  fsplit  8047  xpsnen  8974  elfpw  9238  rankuni  9756  prprrab  14380  isprm2  16593  ismnd  18645  dfgrp2e  18876  pjfval2  21647  neipeltop  23045  cmpfi  23324  isxms2  24364  ishl2  25298  wwlksn0s  29840  clwwlkn1  30019  clwwlkn2  30022  pjimai  32154  bj-snglc  37009  bj-dfid2ALT  37105  bj-epelb  37109  bj-elid6  37210  isbndx  37828  inecmo2  38390  inecmo3  38395  dfrefrel2  38558  dfcnvrefrel2  38573  dfsymrel2  38592  dfsymrel4  38594  dfsymrel5  38595  refsymrels2  38608  refsymrel2  38610  refsymrel3  38611  dftrrel2  38620  elfunsALTV2  38737  elfunsALTV3  38738  elfunsALTV4  38739  elfunsALTV5  38740  eldisjs2  38767  cdlemefrs29pre00  40440  cdlemefrs29cpre1  40443  dihglb2  41387  redvmptabs  42399  elnonrel  43624  pm13.193  44450  dfnbgr6  47894