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  4077  brinxp  5717  copsex2ga  5770  canth  7341  riotaxfrd  7378  iscard  9928  kmlem14  10117  ltxrlt  11244  elioo5  13364  prmind2  16655  pcelnn  16841  isnirred  20329  isdomn3  20624  isreg2  23264  comppfsc  23419  kqcldsat  23620  elmptrab  23714  itg2uba  25644  prmorcht  27088  adjeq  31864  lnopcnbd  31965  cvexchlem  32297  maprnin  32654  topfne  36342  ismblfin  37655  ftc1anclem5  37691  isdmn2  38049  cdlemefrs29pre00  40389  cdlemefrs29cpre1  40392  elmapintab  43585  bits0ALTV  47680