Theorem baibr 541

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  rbaibr  542  pm5.44  547  exmoeub  2584  ssnelpss  4045  brinxp  5697  copsex2ga  5750  canth  7310  riotaxfrd  7347  iscard  9890  kmlem14  10077  ltxrlt  11207  elioo5  13347  prmind2  16645  pcelnn  16832  isnirred  20391  isdomn3  20687  isreg2  23360  comppfsc  23515  kqcldsat  23716  elmptrab  23810  itg2uba  25728  prmorcht  27159  adjeq  32024  lnopcnbd  32125  cvexchlem  32457  maprnin  32823  topfne  36582  ismblfin  38028  ftc1anclem5  38064  isdmn2  38422  cdlemefrs29pre00  40887  cdlemefrs29cpre1  40890  elmapintab  44040  bits0ALTV  48170