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  2600  2eu5  2682  ceqsralt  3487  ceqsrexbv  3613  reuind  3714  rabsn  4685  preqsn  4825  dfiun2g  4992  reusv2lem4  5370  reusv2lem5  5371  dfid2  5556  elidinxp  6044  dfoprab2  7475  fsplit  8118  xpsnen  9063  elfpw  9325  rankuni  9849  prprrab  14542  isprm2  16778  ismnd  18845  dfgrp2e  19093  pjfval2  21928  neipeltop  23360  cmpfi  23639  isxms2  24680  ishl2  25604  wwlksn0s  30337  clwwlkn1  30519  clwwlkn2  30522  pjimai  32665  bj-snglc  37721  bj-dfid2ALT  37817  bj-epelb  37821  bj-elid6  37930  isbndx  38540  inecmo2  39112  inecmo3  39125  dfrefrel2  39351  dfcnvrefrel2  39366  dfsymrel2  39389  dfsymrel4  39391  dfsymrel5  39392  refsymrels2  39405  refsymrel2  39407  refsymrel3  39408  dftrrel2  39417  elfunsALTV2  39534  elfunsALTV3  39535  elfunsALTV4  39536  elfunsALTV5  39537  eldisjs2  39576  cdlemefrs29pre00  41276  cdlemefrs29cpre1  41279  dihglb2  42223  redvmptabs  43243  elnonrel  44433  pm13.193  45243  dfnbgr6  48781  2alsraln0  50754