Theorem baibr 544

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  rbaibr  545  pm5.44  550  exmoeub  2607  ssnelpss  4068  brinxp  5726  copsex2ga  5780  canth  7350  riotaxfrd  7387  iscard  9933  kmlem14  10120  ltxrlt  11253  elioo5  13407  prmind2  16719  pcelnn  16906  isnirred  20469  isdomn3  20765  isreg2  23437  comppfsc  23592  kqcldsat  23793  elmptrab  23887  itg2uba  25805  prmorcht  27242  adjeq  32138  lnopcnbd  32239  cvexchlem  32571  maprnin  32933  topfne  36714  ismblfin  38160  ftc1anclem5  38196  isdmn2  38554  cdlemefrs29pre00  41019  cdlemefrs29cpre1  41022  elmapintab  44172  bits0ALTV  48301