Theorem baibr 943

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm5.44  948  exmoeu2  2485  ssnelpss  3680  brinxp  5104  copsex2ga  5154  canth  6508  riotaxfrd  6541  iscard  8684  kmlem14  8868  ltxrlt  9987  elioo5  12102  prmind2  15236  pcelnn  15412  isnirred  18523  isreg2  20991  comppfsc  21145  kqcldsat  21346  elmptrab  21440  itg2uba  23316  prmorcht  24704  adjeq  28178  lnopcnbd  28279  cvexchlem  28611  maprnin  28894  topfne  31519  ismblfin  32620  ftc1anclem5  32659  isdmn2  33024  cdlemefrs29pre00  34701  cdlemefrs29cpre1  34704  isdomn3  36801  elmapintab  36921  bits0ALTV  40128