Theorem baibr 546

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rbaibr  547  pm5.44  552  exmoeub  2605  ssnelpss  4041  brinxp  5731  copsex2ga  5786  canth  7378  riotaxfrd  7415  iscard  10063  kmlem14  10249  ltxrlt  11387  elioo5  13541  prmind2  16869  pcelnn  17057  isnirred  20659  isdomn3  20975  isreg2  23704  comppfsc  23860  kqcldsat  24061  elmptrab  24155  itg2uba  26073  prmorcht  27514  adjeq  32546  lnopcnbd  32647  cvexchlem  32979  maprnin  33373  srepdflem1  36036  topfne  37266  ismblfin  38716  ftc1anclem5  38752  isdmn2  39126  cdlemefrs29pre00  41589  cdlemefrs29cpre1  41592  elmapintab  44733  bits0ALTV  48913