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  4063  brinxp  5734  copsex2ga  5788  canth  7368  riotaxfrd  7405  iscard  9981  kmlem14  10167  ltxrlt  11305  elioo5  13457  prmind2  16776  pcelnn  16963  isnirred  20562  isdomn3  20877  isreg2  23603  comppfsc  23759  kqcldsat  23960  elmptrab  24054  itg2uba  25972  prmorcht  27415  adjeq  32417  lnopcnbd  32518  cvexchlem  32850  maprnin  33203  topfne  36974  ismblfin  38411  ftc1anclem5  38447  isdmn2  38806  cdlemefrs29pre00  41269  cdlemefrs29cpre1  41272  elmapintab  44437  bits0ALTV  48596