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  2574  2eu5  2657  ceqsralt  3465  ceqsrexbv  3599  reuind  3700  rabsn  4666  preqsn  4806  dfiun2g  4973  reusv2lem4  5338  reusv2lem5  5339  dfid2  5521  elidinxp  6003  dfoprab2  7418  fsplit  8060  xpsnen  8992  elfpw  9257  rankuni  9778  prprrab  14426  isprm2  16642  ismnd  18696  dfgrp2e  18930  pjfval2  21699  neipeltop  23104  cmpfi  23383  isxms2  24423  ishl2  25347  wwlksn0s  29944  clwwlkn1  30126  clwwlkn2  30129  pjimai  32262  bj-snglc  37292  bj-dfid2ALT  37388  bj-epelb  37392  bj-elid6  37500  isbndx  38117  inecmo2  38691  inecmo3  38704  dfrefrel2  38930  dfcnvrefrel2  38945  dfsymrel2  38968  dfsymrel4  38970  dfsymrel5  38971  refsymrels2  38984  refsymrel2  38986  refsymrel3  38987  dftrrel2  38996  elfunsALTV2  39113  elfunsALTV3  39114  elfunsALTV4  39115  elfunsALTV5  39116  eldisjs2  39155  cdlemefrs29pre00  40855  cdlemefrs29cpre1  40858  dihglb2  41802  redvmptabs  42806  elnonrel  44030  pm13.193  44856  dfnbgr6  48345