Theorem baibr 539

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 538	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
3	2	bicomd 225	1 ⊢ (𝜓 → (𝜒 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  rbaibr  540  pm5.44  545  exmoeub  2661  ssnelpss  4087  brinxp  5624  copsex2ga  5674  canth  7105  riotaxfrd  7142  iscard  9398  kmlem14  9583  ltxrlt  10705  elioo5  12788  prmind2  16023  pcelnn  16200  isnirred  19444  isreg2  21979  comppfsc  22134  kqcldsat  22335  elmptrab  22429  itg2uba  24338  prmorcht  25749  adjeq  29706  lnopcnbd  29807  cvexchlem  30139  maprnin  30461  topfne  33697  ismblfin  34927  ftc1anclem5  34965  isdmn2  35327  cdlemefrs29pre00  37525  cdlemefrs29cpre1  37528  isdomn3  39797  elmapintab  39949  bits0ALTV  43838