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  2580  ssnelpss  4114  brinxp  5764  copsex2ga  5817  canth  7385  riotaxfrd  7422  iscard  10015  kmlem14  10204  ltxrlt  11331  elioo5  13444  prmind2  16722  pcelnn  16908  isnirred  20420  isdomn3  20715  isreg2  23385  comppfsc  23540  kqcldsat  23741  elmptrab  23835  itg2uba  25778  prmorcht  27221  adjeq  31954  lnopcnbd  32055  cvexchlem  32387  maprnin  32742  topfne  36355  ismblfin  37668  ftc1anclem5  37704  isdmn2  38062  cdlemefrs29pre00  40397  cdlemefrs29cpre1  40400  elmapintab  43609  bits0ALTV  47666