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  2575  ssnelpss  4059  brinxp  5690  copsex2ga  5742  canth  7295  riotaxfrd  7332  iscard  9863  kmlem14  10050  ltxrlt  11178  elioo5  13298  prmind2  16591  pcelnn  16777  isnirred  20333  isdomn3  20625  isreg2  23287  comppfsc  23442  kqcldsat  23643  elmptrab  23737  itg2uba  25666  prmorcht  27110  adjeq  31907  lnopcnbd  32008  cvexchlem  32340  maprnin  32706  topfne  36388  ismblfin  37701  ftc1anclem5  37737  isdmn2  38095  cdlemefrs29pre00  40434  cdlemefrs29cpre1  40437  elmapintab  43629  bits0ALTV  47710