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  2608  ssnelpss  4069  brinxp  5740  copsex2ga  5794  canth  7364  riotaxfrd  7401  iscard  9957  kmlem14  10143  ltxrlt  11275  elioo5  13425  prmind2  16738  pcelnn  16925  isnirred  20498  isdomn3  20813  isreg2  23534  comppfsc  23689  kqcldsat  23890  elmptrab  23984  itg2uba  25902  prmorcht  27342  adjeq  32287  lnopcnbd  32388  cvexchlem  32720  maprnin  33076  topfne  36865  ismblfin  38312  ftc1anclem5  38348  isdmn2  38706  cdlemefrs29pre00  41169  cdlemefrs29cpre1  41172  elmapintab  44322  bits0ALTV  48444