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  2568  2eu5  2651  ceqsralt  3471  ceqsrexbv  3606  reuind  3707  rabsn  4673  preqsn  4813  dfiun2g  4980  reusv2lem4  5341  reusv2lem5  5342  dfid2  5516  elidinxp  5998  dfoprab2  7410  fsplit  8053  xpsnen  8980  elfpw  9244  rankuni  9762  prprrab  14386  isprm2  16599  ismnd  18651  dfgrp2e  18882  pjfval2  21652  neipeltop  23050  cmpfi  23329  isxms2  24369  ishl2  25303  wwlksn0s  29846  clwwlkn1  30028  clwwlkn2  30031  pjimai  32163  bj-snglc  37020  bj-dfid2ALT  37116  bj-epelb  37120  bj-elid6  37221  isbndx  37828  inecmo2  38394  inecmo3  38399  dfrefrel2  38613  dfcnvrefrel2  38628  dfsymrel2  38651  dfsymrel4  38653  dfsymrel5  38654  refsymrels2  38667  refsymrel2  38669  refsymrel3  38670  dftrrel2  38679  elfunsALTV2  38797  elfunsALTV3  38798  elfunsALTV4  38799  elfunsALTV5  38800  eldisjs2  38827  cdlemefrs29pre00  40500  cdlemefrs29cpre1  40503  dihglb2  41447  redvmptabs  42459  elnonrel  43683  pm13.193  44509  dfnbgr6  47962