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  2573  2eu5  2656  ceqsralt  3475  ceqsrexbv  3610  reuind  3711  rabsn  4678  preqsn  4818  dfiun2g  4985  reusv2lem4  5346  reusv2lem5  5347  dfid2  5521  elidinxp  6003  dfoprab2  7416  fsplit  8059  xpsnen  8989  elfpw  9254  rankuni  9775  prprrab  14396  isprm2  16609  ismnd  18662  dfgrp2e  18893  pjfval2  21664  neipeltop  23073  cmpfi  23352  isxms2  24392  ishl2  25326  wwlksn0s  29934  clwwlkn1  30116  clwwlkn2  30119  pjimai  32251  bj-snglc  37170  bj-dfid2ALT  37266  bj-epelb  37270  bj-elid6  37375  isbndx  37983  inecmo2  38549  inecmo3  38554  dfrefrel2  38768  dfcnvrefrel2  38783  dfsymrel2  38806  dfsymrel4  38808  dfsymrel5  38809  refsymrels2  38822  refsymrel2  38824  refsymrel3  38825  dftrrel2  38834  elfunsALTV2  38952  elfunsALTV3  38953  elfunsALTV4  38954  elfunsALTV5  38955  eldisjs2  38982  cdlemefrs29pre00  40655  cdlemefrs29cpre1  40658  dihglb2  41602  redvmptabs  42615  elnonrel  43826  pm13.193  44652  dfnbgr6  48103