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  2606  ssnelpss  4063  brinxp  5730  copsex2ga  5785  canth  7374  riotaxfrd  7411  iscard  10056  kmlem14  10242  ltxrlt  11380  elioo5  13534  prmind2  16860  pcelnn  17048  isnirred  20650  isdomn3  20966  isreg2  23695  comppfsc  23851  kqcldsat  24052  elmptrab  24146  itg2uba  26064  prmorcht  27505  adjeq  32537  lnopcnbd  32638  cvexchlem  32970  maprnin  33323  topfne  37142  ismblfin  38579  ftc1anclem5  38615  isdmn2  38989  cdlemefrs29pre00  41452  cdlemefrs29cpre1  41455  elmapintab  44595  bits0ALTV  48776