Theorem baibr 537

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  rbaibr  538  pm5.44  543  exmoeub  2580  ssnelpss  4046  brinxp  5665  copsex2ga  5717  canth  7229  riotaxfrd  7267  iscard  9733  kmlem14  9919  ltxrlt  11045  elioo5  13136  prmind2  16390  pcelnn  16571  isnirred  19942  isreg2  22528  comppfsc  22683  kqcldsat  22884  elmptrab  22978  itg2uba  24908  prmorcht  26327  adjeq  30297  lnopcnbd  30398  cvexchlem  30730  maprnin  31066  topfne  34543  ismblfin  35818  ftc1anclem5  35854  isdmn2  36213  cdlemefrs29pre00  38409  cdlemefrs29cpre1  38412  isdomn3  41029  elmapintab  41204  bits0ALTV  45131