Theorem pm5.32ri 575

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bianim  576  anbi1i  624  pm5.36  833  oranabs  1001  pm5.61  1002  pm5.75  1030  eu6lem  2572  2eu5  2655  ceqsralt  3495  ceqsrexbv  3635  reuind  3736  rabsn  4697  preqsn  4838  dfiun2g  5006  reusv2lem4  5371  reusv2lem5  5372  dfid2  5550  elidinxp  6031  dfoprab2  7465  fsplit  8116  xpsnen  9069  elfpw  9366  rankuni  9877  prprrab  14491  isprm2  16701  ismnd  18715  dfgrp2e  18946  pjfval2  21669  neipeltop  23067  cmpfi  23346  isxms2  24387  ishl2  25322  wwlksn0s  29843  clwwlkn1  30022  clwwlkn2  30025  pjimai  32157  bj-snglc  36987  bj-dfid2ALT  37083  bj-epelb  37087  bj-elid6  37188  isbndx  37806  inecmo2  38374  inecmo3  38379  dfrefrel2  38533  dfcnvrefrel2  38548  dfsymrel2  38567  dfsymrel4  38569  dfsymrel5  38570  refsymrels2  38583  refsymrel2  38585  refsymrel3  38586  dftrrel2  38595  elfunsALTV2  38711  elfunsALTV3  38712  elfunsALTV4  38713  elfunsALTV5  38714  eldisjs2  38741  cdlemefrs29pre00  40414  cdlemefrs29cpre1  40417  dihglb2  41361  redvmptabs  42403  elnonrel  43609  pm13.193  44435  dfnbgr6  47870