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 302	1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi1i  623  pm5.36  830  oranabs  996  pm5.61  997  pm5.75  1025  eu6lem  2573  2eu5  2657  ceqsralt  3453  ceqsrexbv  3579  reuind  3683  rabsn  4654  preqsn  4789  reusv2lem4  5319  reusv2lem5  5320  dfid2  5482  elidinxp  5940  dfoprab2  7311  fsplit  7928  fsplitOLD  7929  xpsnen  8796  elfpw  9051  rankuni  9552  prprrab  14115  isprm2  16315  ismnd  18303  dfgrp2e  18520  pjfval2  20826  neipeltop  22188  cmpfi  22467  isxms2  23509  ishl2  24439  wwlksn0s  28127  clwwlkn1  28306  clwwlkn2  28309  pjimai  30439  bj-snglc  35086  bj-dfid2ALT  35163  bj-epelb  35167  bj-elid6  35268  isbndx  35867  inecmo2  36415  inecmo3  36420  dfrefrel2  36560  dfcnvrefrel2  36573  dfsymrel2  36590  dfsymrel4  36592  dfsymrel5  36593  refsymrels2  36606  refsymrel2  36608  refsymrel3  36609  dftrrel2  36618  elfunsALTV2  36731  elfunsALTV3  36732  elfunsALTV4  36733  elfunsALTV5  36734  eldisjs2  36761  cdlemefrs29pre00  38336  cdlemefrs29cpre1  38339  dihglb2  39283  elnonrel  41082  pm13.193  41918