Theorem baibr 545

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rbaibr  546  pm5.44  551  exmoeub  2614  ssnelpss  4077  brinxp  5741  copsex2ga  5795  canth  7365  riotaxfrd  7402  iscard  9960  kmlem14  10146  ltxrlt  11279  elioo5  13429  prmind2  16742  pcelnn  16929  isnirred  20501  isdomn3  20798  isreg2  23502  comppfsc  23657  kqcldsat  23858  elmptrab  23952  itg2uba  25870  prmorcht  27307  adjeq  32227  lnopcnbd  32328  cvexchlem  32660  maprnin  33016  topfne  36753  ismblfin  38199  ftc1anclem5  38235  isdmn2  38593  cdlemefrs29pre00  41058  cdlemefrs29cpre1  41061  elmapintab  44213  bits0ALTV  48332