Theorem rbaib 538

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 537	. 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:  pm5.75  1030  cador  1608  reusv1  5339  reusv2lem1  5340  fpwwe2  10556  fzsplit2  13470  saddisjlem  16393  smupval  16417  smueqlem  16419  prmrec  16852  ablnsg  19744  cnprest  23192  flimrest  23886  fclsrest  23927  tsmssubm  24046  setsxms  24383  tcphcph  25153  ellimc2  25794  fsumvma2  27141  chpub  27147  mdbr2  32258  mdsl2i  32284  fzsplit3  32749  posrasymb  32922  trleile  32926  fvineqsneu  37384  cnvcnvintabd  43573  grumnud  44259  mofeu  48833