Theorem baibr 540

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  rbaibr  541  pm5.44  546  exmoeub  2579  ssnelpss  4026  brinxp  5627  copsex2ga  5677  canth  7167  riotaxfrd  7205  iscard  9591  kmlem14  9777  ltxrlt  10903  elioo5  12992  prmind2  16242  pcelnn  16423  isnirred  19718  isreg2  22274  comppfsc  22429  kqcldsat  22630  elmptrab  22724  itg2uba  24641  prmorcht  26060  adjeq  30016  lnopcnbd  30117  cvexchlem  30449  maprnin  30786  topfne  34280  ismblfin  35555  ftc1anclem5  35591  isdmn2  35950  cdlemefrs29pre00  38146  cdlemefrs29cpre1  38149  isdomn3  40732  elmapintab  40880  bits0ALTV  44804