Theorem baibr 536

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  rbaibr  537  pm5.44  542  exmoeub  2580  ssnelpss  4042  brinxp  5656  copsex2ga  5706  canth  7209  riotaxfrd  7247  iscard  9664  kmlem14  9850  ltxrlt  10976  elioo5  13065  prmind2  16318  pcelnn  16499  isnirred  19857  isreg2  22436  comppfsc  22591  kqcldsat  22792  elmptrab  22886  itg2uba  24813  prmorcht  26232  adjeq  30198  lnopcnbd  30299  cvexchlem  30631  maprnin  30968  topfne  34470  ismblfin  35745  ftc1anclem5  35781  isdmn2  36140  cdlemefrs29pre00  38336  cdlemefrs29cpre1  38339  isdomn3  40945  elmapintab  41093  bits0ALTV  45019