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  2574  ssnelpss  4080  brinxp  5720  copsex2ga  5773  canth  7344  riotaxfrd  7381  iscard  9935  kmlem14  10124  ltxrlt  11251  elioo5  13371  prmind2  16662  pcelnn  16848  isnirred  20336  isdomn3  20631  isreg2  23271  comppfsc  23426  kqcldsat  23627  elmptrab  23721  itg2uba  25651  prmorcht  27095  adjeq  31871  lnopcnbd  31972  cvexchlem  32304  maprnin  32661  topfne  36349  ismblfin  37662  ftc1anclem5  37698  isdmn2  38056  cdlemefrs29pre00  40396  cdlemefrs29cpre1  40399  elmapintab  43592  bits0ALTV  47684