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 223	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:  rbaibr  537  pm5.44  542  exmoeub  2583  ssnelpss  4137  brinxp  5778  copsex2ga  5831  canth  7401  riotaxfrd  7439  iscard  10044  kmlem14  10233  ltxrlt  11360  elioo5  13464  prmind2  16732  pcelnn  16917  isnirred  20446  isdomn3  20737  isreg2  23406  comppfsc  23561  kqcldsat  23762  elmptrab  23856  itg2uba  25798  prmorcht  27239  adjeq  31967  lnopcnbd  32068  cvexchlem  32400  maprnin  32745  topfne  36320  ismblfin  37621  ftc1anclem5  37657  isdmn2  38015  cdlemefrs29pre00  40352  cdlemefrs29cpre1  40355  elmapintab  43558  bits0ALTV  47553