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  2573  ssnelpss  4065  brinxp  5698  copsex2ga  5750  canth  7303  riotaxfrd  7340  iscard  9871  kmlem14  10058  ltxrlt  11186  elioo5  13306  prmind2  16596  pcelnn  16782  isnirred  20305  isdomn3  20600  isreg2  23262  comppfsc  23417  kqcldsat  23618  elmptrab  23712  itg2uba  25642  prmorcht  27086  adjeq  31879  lnopcnbd  31980  cvexchlem  32312  maprnin  32674  topfne  36328  ismblfin  37641  ftc1anclem5  37677  isdmn2  38035  cdlemefrs29pre00  40374  cdlemefrs29cpre1  40377  elmapintab  43569  bits0ALTV  47663