Theorem pm5.32ri 586

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianim  587  anbi1i  636  pm5.36  847  oranabs  1015  pm5.61  1016  pm5.75  1046  eu6lem  2604  2eu5  2686  ceqsralt  3492  ceqsrexbv  3618  reuind  3719  rabsn  4692  preqsn  4832  dfiun2g  4999  reusv2lem4  5377  reusv2lem5  5378  dfid2  5563  elidinxp  6051  dfoprab2  7481  fsplit  8121  xpsnen  9059  elfpw  9321  rankuni  9845  prprrab  14530  isprm2  16765  ismnd  18824  dfgrp2e  19061  pjfval2  21896  neipeltop  23323  cmpfi  23602  isxms2  24642  ishl2  25566  wwlksn0s  30247  clwwlkn1  30429  clwwlkn2  30432  pjimai  32565  bj-snglc  37646  bj-dfid2ALT  37742  bj-epelb  37746  bj-elid6  37855  isbndx  38474  inecmo2  39046  inecmo3  39059  dfrefrel2  39285  dfcnvrefrel2  39300  dfsymrel2  39323  dfsymrel4  39325  dfsymrel5  39326  refsymrels2  39339  refsymrel2  39341  refsymrel3  39342  dftrrel2  39351  elfunsALTV2  39468  elfunsALTV3  39469  elfunsALTV4  39470  elfunsALTV5  39471  eldisjs2  39510  cdlemefrs29pre00  41210  cdlemefrs29cpre1  41213  dihglb2  42157  redvmptabs  43162  elnonrel  44352  pm13.193  45162  dfnbgr6  48663  2alsraln0  50636