Theorem rbaib 542

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm5.75  1026  cador  1610  reusv1  5263  reusv2lem1  5264  fpwwe2  10054  fzsplit2  12927  saddisjlem  15803  smupval  15827  smueqlem  15829  prmrec  16248  ablnsg  18960  cnprest  21894  flimrest  22588  fclsrest  22629  tsmssubm  22748  setsxms  23086  tcphcph  23841  ellimc2  24480  fsumvma2  25798  chpub  25804  mdbr2  30079  mdsl2i  30105  fzsplit3  30543  posrasymb  30670  trleile  30679  fvineqsneu  34828  cnvcnvintabd  40300  grumnud  40994