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  625  pm5.36  834  oranabs  1002  pm5.61  1003  pm5.75  1031  eu6lem  2573  2eu5  2656  ceqsralt  3464  ceqsrexbv  3598  reuind  3699  rabsn  4665  preqsn  4805  dfiun2g  4972  reusv2lem4  5343  reusv2lem5  5344  dfid2  5528  elidinxp  6009  dfoprab2  7425  fsplit  8067  xpsnen  8999  elfpw  9264  rankuni  9787  prprrab  14435  isprm2  16651  ismnd  18705  dfgrp2e  18939  pjfval2  21689  neipeltop  23094  cmpfi  23373  isxms2  24413  ishl2  25337  wwlksn0s  29929  clwwlkn1  30111  clwwlkn2  30114  pjimai  32247  bj-snglc  37276  bj-dfid2ALT  37372  bj-epelb  37376  bj-elid6  37484  isbndx  38103  inecmo2  38677  inecmo3  38690  dfrefrel2  38916  dfcnvrefrel2  38931  dfsymrel2  38954  dfsymrel4  38956  dfsymrel5  38957  refsymrels2  38970  refsymrel2  38972  refsymrel3  38973  dftrrel2  38982  elfunsALTV2  39099  elfunsALTV3  39100  elfunsALTV4  39101  elfunsALTV5  39102  eldisjs2  39141  cdlemefrs29pre00  40841  cdlemefrs29cpre1  40844  dihglb2  41788  redvmptabs  42792  elnonrel  44012  pm13.193  44838  dfnbgr6  48333