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  2577  ssnelpss  4063  brinxp  5700  copsex2ga  5753  canth  7309  riotaxfrd  7346  iscard  9879  kmlem14  10066  ltxrlt  11194  elioo5  13310  prmind2  16603  pcelnn  16789  isnirred  20347  isdomn3  20639  isreg2  23312  comppfsc  23467  kqcldsat  23668  elmptrab  23762  itg2uba  25691  prmorcht  27135  adjeq  31936  lnopcnbd  32037  cvexchlem  32369  maprnin  32738  topfne  36470  ismblfin  37774  ftc1anclem5  37810  isdmn2  38168  cdlemefrs29pre00  40567  cdlemefrs29cpre1  40570  elmapintab  43753  bits0ALTV  47841