Theorem baibr 526

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  pm5.44  532  exmoeu2  2645  ssnelpss  3868  brinxp  5321  copsex2ga  5370  canth  6751  riotaxfrd  6785  iscard  9001  kmlem14  9187  ltxrlt  10310  elioo5  12436  prmind2  15605  pcelnn  15781  isnirred  18908  isreg2  21402  comppfsc  21556  kqcldsat  21757  elmptrab  21851  itg2uba  23730  prmorcht  25125  adjeq  29134  lnopcnbd  29235  cvexchlem  29567  maprnin  29846  topfne  32686  ismblfin  33783  ftc1anclem5  33821  isdmn2  34186  cdlemefrs29pre00  36204  cdlemefrs29cpre1  36207  isdomn3  38308  elmapintab  38428  bits0ALTV  42118