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  2578  ssnelpss  4124  brinxp  5767  copsex2ga  5820  canth  7385  riotaxfrd  7422  iscard  10013  kmlem14  10202  ltxrlt  11329  elioo5  13441  prmind2  16719  pcelnn  16904  isnirred  20437  isdomn3  20732  isreg2  23401  comppfsc  23556  kqcldsat  23757  elmptrab  23851  itg2uba  25793  prmorcht  27236  adjeq  31964  lnopcnbd  32065  cvexchlem  32397  maprnin  32749  topfne  36337  ismblfin  37648  ftc1anclem5  37684  isdmn2  38042  cdlemefrs29pre00  40378  cdlemefrs29cpre1  40381  elmapintab  43586  bits0ALTV  47604