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  5266  reusv2lem1  5267  fpwwe2  10103  fzsplit2  12981  saddisjlem  15863  smupval  15887  smueqlem  15889  prmrec  16313  ablnsg  19035  cnprest  21989  flimrest  22683  fclsrest  22724  tsmssubm  22843  setsxms  23181  tcphcph  23937  ellimc2  24576  fsumvma2  25897  chpub  25903  mdbr2  30178  mdsl2i  30204  fzsplit3  30639  posrasymb  30766  trleile  30775  fvineqsneu  35108  cnvcnvintabd  40673  grumnud  41367