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:  anbi1i  623  pm5.36  833  oranabs  1000  pm5.61  1001  pm5.75  1029  eu6lem  2576  2eu5  2659  ceqsralt  3524  ceqsrexbv  3669  reuind  3775  rabsn  4746  preqsn  4886  dfiun2g  5053  reusv2lem4  5419  reusv2lem5  5420  dfid2  5595  elidinxp  6073  dfoprab2  7508  fsplit  8158  xpsnen  9121  elfpw  9424  rankuni  9932  prprrab  14522  isprm2  16729  ismnd  18775  dfgrp2e  19003  pjfval2  21752  neipeltop  23158  cmpfi  23437  isxms2  24479  ishl2  25423  wwlksn0s  29894  clwwlkn1  30073  clwwlkn2  30076  pjimai  32208  bj-snglc  36935  bj-dfid2ALT  37031  bj-epelb  37035  bj-elid6  37136  isbndx  37742  bianim  38185  inecmo2  38312  inecmo3  38317  dfrefrel2  38471  dfcnvrefrel2  38486  dfsymrel2  38505  dfsymrel4  38507  dfsymrel5  38508  refsymrels2  38521  refsymrel2  38523  refsymrel3  38524  dftrrel2  38533  elfunsALTV2  38649  elfunsALTV3  38650  elfunsALTV4  38651  elfunsALTV5  38652  eldisjs2  38679  cdlemefrs29pre00  40352  cdlemefrs29cpre1  40355  dihglb2  41299  elnonrel  43547  pm13.193  44380  dfnbgr6  47729