Theorem pm5.32ri 576

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 575	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))
3		ancom 461	. 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓))
4		ancom 461	. 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜑 ∧ 𝜒))
5	2, 3, 4	3bitr4i 303	1 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anbi1i  624  pm5.36  831  oranabs  997  pm5.61  998  pm5.75  1026  eu6lem  2573  2eu5  2657  ceqsralt  3463  ceqsrexbv  3586  reuind  3688  rabsn  4657  preqsn  4792  dfiun2g  4960  reusv2lem4  5324  reusv2lem5  5325  dfid2  5491  elidinxp  5951  dfoprab2  7333  fsplit  7957  fsplitOLD  7958  xpsnen  8842  elfpw  9121  rankuni  9621  prprrab  14187  isprm2  16387  ismnd  18388  dfgrp2e  18605  pjfval2  20916  neipeltop  22280  cmpfi  22559  isxms2  23601  ishl2  24534  wwlksn0s  28226  clwwlkn1  28405  clwwlkn2  28408  pjimai  30538  bj-snglc  35159  bj-dfid2ALT  35236  bj-epelb  35240  bj-elid6  35341  isbndx  35940  inecmo2  36488  inecmo3  36493  dfrefrel2  36633  dfcnvrefrel2  36646  dfsymrel2  36663  dfsymrel4  36665  dfsymrel5  36666  refsymrels2  36679  refsymrel2  36681  refsymrel3  36682  dftrrel2  36691  elfunsALTV2  36804  elfunsALTV3  36805  elfunsALTV4  36806  elfunsALTV5  36807  eldisjs2  36834  cdlemefrs29pre00  38409  cdlemefrs29cpre1  38412  dihglb2  39356  elnonrel  41193  pm13.193  42029