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  830  oranabs  996  pm5.61  997  pm5.75  1025  eu6lem  2565  2eu5  2649  ceqsralt  3505  ceqsrexbv  3643  reuind  3748  rabsn  4724  preqsn  4861  dfiun2g  5032  reusv2lem4  5398  reusv2lem5  5399  dfid2  5575  elidinxp  6042  dfoprab2  7469  fsplit  8105  xpsnen  9057  elfpw  9356  rankuni  9860  prprrab  14438  isprm2  16623  ismnd  18662  dfgrp2e  18884  pjfval2  21483  neipeltop  22853  cmpfi  23132  isxms2  24174  ishl2  25118  wwlksn0s  29382  clwwlkn1  29561  clwwlkn2  29564  pjimai  31696  bj-snglc  36153  bj-dfid2ALT  36249  bj-epelb  36253  bj-elid6  36354  isbndx  36953  bianim  37399  inecmo2  37528  inecmo3  37533  dfrefrel2  37688  dfcnvrefrel2  37703  dfsymrel2  37722  dfsymrel4  37724  dfsymrel5  37725  refsymrels2  37738  refsymrel2  37740  refsymrel3  37741  dftrrel2  37750  elfunsALTV2  37866  elfunsALTV3  37867  elfunsALTV4  37868  elfunsALTV5  37869  eldisjs2  37896  cdlemefrs29pre00  39569  cdlemefrs29cpre1  39572  dihglb2  40516  elnonrel  42638  pm13.193  43472