Theorem baibr 965

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm5.44  970  exmoeu2  2525  ssnelpss  3751  brinxp  5215  copsex2ga  5264  canth  6648  riotaxfrd  6682  iscard  8839  kmlem14  9023  ltxrlt  10146  elioo5  12269  prmind2  15445  pcelnn  15621  isnirred  18746  isreg2  21229  comppfsc  21383  kqcldsat  21584  elmptrab  21678  itg2uba  23555  prmorcht  24949  adjeq  28922  lnopcnbd  29023  cvexchlem  29355  maprnin  29634  topfne  32474  ismblfin  33580  ftc1anclem5  33619  isdmn2  33984  cdlemefrs29pre00  36000  cdlemefrs29cpre1  36003  isdomn3  38099  elmapintab  38219  bits0ALTV  41915