Theorem baibr 546

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rbaibr  547  pm5.44  552  exmoeub  2610  ssnelpss  4070  brinxp  5742  copsex2ga  5796  canth  7373  riotaxfrd  7410  iscard  9977  kmlem14  10163  ltxrlt  11295  elioo5  13446  prmind2  16765  pcelnn  16952  isnirred  20548  isdomn3  20863  isreg2  23584  comppfsc  23740  kqcldsat  23941  elmptrab  24035  itg2uba  25953  prmorcht  27393  adjeq  32358  lnopcnbd  32459  cvexchlem  32791  maprnin  33146  topfne  36922  ismblfin  38369  ftc1anclem5  38405  isdmn2  38764  cdlemefrs29pre00  41227  cdlemefrs29cpre1  41230  elmapintab  44380  bits0ALTV  48502