Theorem baibr 536

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rbaibr  537  pm5.44  542  exmoeub  2580  ssnelpss  4066  brinxp  5703  copsex2ga  5756  canth  7312  riotaxfrd  7349  iscard  9887  kmlem14  10074  ltxrlt  11203  elioo5  13319  prmind2  16612  pcelnn  16798  isnirred  20356  isdomn3  20648  isreg2  23321  comppfsc  23476  kqcldsat  23677  elmptrab  23771  itg2uba  25700  prmorcht  27144  adjeq  32010  lnopcnbd  32111  cvexchlem  32443  maprnin  32810  topfne  36548  ismblfin  37862  ftc1anclem5  37898  isdmn2  38256  cdlemefrs29pre00  40655  cdlemefrs29cpre1  40658  elmapintab  43837  bits0ALTV  47925