Theorem baibr 944

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  pm5.44  949  exmoeu2  2495  ssnelpss  3710  brinxp  5171  copsex2ga  5221  canth  6593  riotaxfrd  6627  iscard  8786  kmlem14  8970  ltxrlt  10093  elioo5  12216  prmind2  15379  pcelnn  15555  isnirred  18681  isreg2  21162  comppfsc  21316  kqcldsat  21517  elmptrab  21611  itg2uba  23491  prmorcht  24885  adjeq  28764  lnopcnbd  28865  cvexchlem  29197  maprnin  29480  topfne  32324  ismblfin  33421  ftc1anclem5  33460  isdmn2  33825  cdlemefrs29pre00  35502  cdlemefrs29cpre1  35505  isdomn3  37601  elmapintab  37721  bits0ALTV  41355