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  5367  reusv2lem1  5368  fpwwe2  10657  fzsplit2  13566  saddisjlem  16483  smupval  16507  smueqlem  16509  prmrec  16942  ablnsg  19828  cnprest  23227  flimrest  23921  fclsrest  23962  tsmssubm  24081  setsxms  24418  tcphcph  25189  ellimc2  25830  fsumvma2  27177  chpub  27183  mdbr2  32277  mdsl2i  32303  fzsplit3  32770  posrasymb  32945  trleile  32951  fvineqsneu  37429  cnvcnvintabd  43624  grumnud  44310  mofeu  48826