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  2599  2eu5  2681  ceqsralt  3485  ceqsrexbv  3610  reuind  3711  rabsn  4682  preqsn  4822  dfiun2g  4988  reusv2lem4  5363  reusv2lem5  5364  dfid2  5548  elidinxp  6038  dfoprab2  7470  fsplit  8117  xpsnen  9064  elfpw  9327  rankuni  9860  prprrab  14598  isprm2  16837  ismnd  18906  dfgrp2e  19154  pjfval2  21995  neipeltop  23427  cmpfi  23706  isxms2  24747  ishl2  25671  wwlksn0s  30432  clwwlkn1  30614  clwwlkn2  30617  pjimai  32760  bj-snglc  37852  bj-dfid2ALT  37948  bj-epelb  37952  bj-elid6  38059  isbndx  38684  inecmo2  39256  inecmo3  39269  dfrefrel2  39495  dfcnvrefrel2  39510  dfsymrel2  39533  dfsymrel4  39535  dfsymrel5  39536  refsymrels2  39549  refsymrel2  39551  refsymrel3  39552  dftrrel2  39561  elfunsALTV2  39678  elfunsALTV3  39679  elfunsALTV4  39680  elfunsALTV5  39681  eldisjs2  39720  cdlemefrs29pre00  41420  cdlemefrs29cpre1  41423  dihglb2  42367  redvmptabs  43379  elnonrel  44544  pm13.193  45354  dfnbgr6  48899  2alsraln0  50857