Theorem pm5.32ri 574

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

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

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 395

This theorem is referenced by:  anbi1i  622  pm5.36  832  oranabs  997  pm5.61  998  pm5.75  1026  eu6lem  2562  2eu5  2647  ceqsralt  3506  ceqsrexbv  3644  reuind  3750  rabsn  4730  preqsn  4867  dfiun2g  5037  reusv2lem4  5405  reusv2lem5  5406  dfid2  5582  elidinxp  6052  dfoprab2  7485  fsplit  8130  xpsnen  9088  elfpw  9388  rankuni  9896  prprrab  14476  isprm2  16662  ismnd  18706  dfgrp2e  18934  pjfval2  21657  neipeltop  23061  cmpfi  23340  isxms2  24382  ishl2  25326  wwlksn0s  29700  clwwlkn1  29879  clwwlkn2  29882  pjimai  32014  bj-snglc  36489  bj-dfid2ALT  36585  bj-epelb  36589  bj-elid6  36690  isbndx  37296  bianim  37741  inecmo2  37868  inecmo3  37873  dfrefrel2  38027  dfcnvrefrel2  38042  dfsymrel2  38061  dfsymrel4  38063  dfsymrel5  38064  refsymrels2  38077  refsymrel2  38079  refsymrel3  38080  dftrrel2  38089  elfunsALTV2  38205  elfunsALTV3  38206  elfunsALTV4  38207  elfunsALTV5  38208  eldisjs2  38235  cdlemefrs29pre00  39908  cdlemefrs29cpre1  39911  dihglb2  40855  elnonrel  43064  pm13.193  43897  dfnbgr6  47239