Theorem rbaib 541

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm5.75  1025  cador  1609  reusv1  5300  reusv2lem1  5301  fpwwe2  10067  fzsplit2  12935  saddisjlem  15815  smupval  15839  smueqlem  15841  prmrec  16260  ablnsg  18969  cnprest  21899  flimrest  22593  fclsrest  22634  tsmssubm  22753  setsxms  23091  tcphcph  23842  ellimc2  24477  fsumvma2  25792  chpub  25798  mdbr2  30075  mdsl2i  30101  fzsplit3  30519  posrasymb  30646  trleile  30655  fvineqsneu  34694  cnvcnvintabd  39967  grumnud  40629