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  4054  brinxp  5710  copsex2ga  5763  canth  7321  riotaxfrd  7358  iscard  9899  kmlem14  10086  ltxrlt  11216  elioo5  13356  prmind2  16654  pcelnn  16841  isnirred  20400  isdomn3  20692  isreg2  23342  comppfsc  23497  kqcldsat  23698  elmptrab  23792  itg2uba  25710  prmorcht  27141  adjeq  32006  lnopcnbd  32107  cvexchlem  32439  maprnin  32804  topfne  36536  ismblfin  37982  ftc1anclem5  38018  isdmn2  38376  cdlemefrs29pre00  40841  cdlemefrs29cpre1  40844  elmapintab  44023  bits0ALTV  48155