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  2608  ssnelpss  4045  brinxp  5738  copsex2ga  5794  canth  7405  riotaxfrd  7442  iscard  10093  kmlem14  10281  ltxrlt  11419  elioo5  13574  prmind2  16904  pcelnn  17092  isnirred  20701  isdomn3  21017  isreg2  23750  comppfsc  23906  kqcldsat  24107  elmptrab  24201  itg2uba  26119  prmorcht  27562  adjeq  32594  lnopcnbd  32695  cvexchlem  33027  maprnin  33419  srepdflem1  36126  topfne  37357  ismblfin  38847  ftc1anclem5  38883  isdmn2  39255  cdlemefrs29pre00  41718  cdlemefrs29cpre1  41721  elmapintab  44857  bits0ALTV  49050