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  2570  2eu5  2653  ceqsralt  3472  ceqsrexbv  3607  reuind  3708  rabsn  4675  preqsn  4815  dfiun2g  4982  reusv2lem4  5343  reusv2lem5  5344  dfid2  5518  elidinxp  5999  dfoprab2  7412  fsplit  8055  xpsnen  8983  elfpw  9247  rankuni  9765  prprrab  14384  isprm2  16597  ismnd  18649  dfgrp2e  18880  pjfval2  21650  neipeltop  23047  cmpfi  23326  isxms2  24366  ishl2  25300  wwlksn0s  29843  clwwlkn1  30025  clwwlkn2  30028  pjimai  32160  bj-snglc  37036  bj-dfid2ALT  37132  bj-epelb  37136  bj-elid6  37237  isbndx  37845  inecmo2  38411  inecmo3  38416  dfrefrel2  38630  dfcnvrefrel2  38645  dfsymrel2  38668  dfsymrel4  38670  dfsymrel5  38671  refsymrels2  38684  refsymrel2  38686  refsymrel3  38687  dftrrel2  38696  elfunsALTV2  38814  elfunsALTV3  38815  elfunsALTV4  38816  elfunsALTV5  38817  eldisjs2  38844  cdlemefrs29pre00  40517  cdlemefrs29cpre1  40520  dihglb2  41464  redvmptabs  42481  elnonrel  43705  pm13.193  44531  dfnbgr6  47984