Theorem baibr 537

Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
baibr	⊢ (𝜓 → (𝜒 ↔ 𝜑))

Proof of Theorem baibr

Step	Hyp	Ref	Expression
1		baib.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	baib 536	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
3	2	bicomd 224	1 ⊢ (𝜓 → (𝜒 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  rbaibr  538  pm5.44  543  exmoeub  2625  ssnelpss  4013  brinxp  5521  copsex2ga  5571  canth  6979  riotaxfrd  7013  iscard  9255  kmlem14  9440  ltxrlt  10563  elioo5  12649  prmind2  15863  pcelnn  16040  isnirred  19145  isreg2  21674  comppfsc  21829  kqcldsat  22030  elmptrab  22124  itg2uba  24032  prmorcht  25442  adjeq  29408  lnopcnbd  29509  cvexchlem  29841  maprnin  30160  topfne  33317  ismblfin  34489  ftc1anclem5  34527  isdmn2  34890  cdlemefrs29pre00  37087  cdlemefrs29cpre1  37090  isdomn3  39314  elmapintab  39466  bits0ALTV  43352