Theorem rbaib 537

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
rbaib	⊢ (𝜒 → (𝜑 ↔ 𝜓))

Proof of Theorem rbaib

Step	Hyp	Ref	Expression
1		baib.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	rbaibr 536	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑))
3	2	bicomd 222	1 ⊢ (𝜒 → (𝜑 ↔ 𝜓))

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

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 395

This theorem is referenced by:  pm5.75  1026  cador  1601  reusv1  5400  reusv2lem1  5401  fpwwe2  10682  fzsplit2  13575  saddisjlem  16459  smupval  16483  smueqlem  16485  prmrec  16919  ablnsg  19840  cnprest  23276  flimrest  23970  fclsrest  24011  tsmssubm  24130  setsxms  24470  tcphcph  25248  ellimc2  25889  fsumvma2  27235  chpub  27241  mdbr2  32221  mdsl2i  32247  fzsplit3  32685  posrasymb  32823  trleile  32829  fvineqsneu  37066  cnvcnvintabd  43204  grumnud  43897  mofeu  48152