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  2579  ssnelpss  4089  brinxp  5733  copsex2ga  5786  canth  7359  riotaxfrd  7396  iscard  9989  kmlem14  10178  ltxrlt  11305  elioo5  13420  prmind2  16704  pcelnn  16890  isnirred  20380  isdomn3  20675  isreg2  23315  comppfsc  23470  kqcldsat  23671  elmptrab  23765  itg2uba  25696  prmorcht  27140  adjeq  31916  lnopcnbd  32017  cvexchlem  32349  maprnin  32708  topfne  36372  ismblfin  37685  ftc1anclem5  37721  isdmn2  38079  cdlemefrs29pre00  40414  cdlemefrs29cpre1  40417  elmapintab  43620  bits0ALTV  47693