Theorem baibr 536

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rbaibr  537  pm5.44  542  exmoeub  2573  ssnelpss  4073  brinxp  5710  copsex2ga  5761  canth  7323  riotaxfrd  7360  iscard  9904  kmlem14  10093  ltxrlt  11220  elioo5  13340  prmind2  16631  pcelnn  16817  isnirred  20305  isdomn3  20600  isreg2  23240  comppfsc  23395  kqcldsat  23596  elmptrab  23690  itg2uba  25620  prmorcht  27064  adjeq  31837  lnopcnbd  31938  cvexchlem  32270  maprnin  32627  topfne  36315  ismblfin  37628  ftc1anclem5  37664  isdmn2  38022  cdlemefrs29pre00  40362  cdlemefrs29cpre1  40365  elmapintab  43558  bits0ALTV  47653