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  2581  ssnelpss  4068  brinxp  5711  copsex2ga  5764  canth  7322  riotaxfrd  7359  iscard  9899  kmlem14  10086  ltxrlt  11215  elioo5  13331  prmind2  16624  pcelnn  16810  isnirred  20368  isdomn3  20660  isreg2  23333  comppfsc  23488  kqcldsat  23689  elmptrab  23783  itg2uba  25712  prmorcht  27156  adjeq  32023  lnopcnbd  32124  cvexchlem  32456  maprnin  32821  topfne  36570  ismblfin  37912  ftc1anclem5  37948  isdmn2  38306  cdlemefrs29pre00  40771  cdlemefrs29cpre1  40774  elmapintab  43952  bits0ALTV  48039