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  1609  reusv1  5335  reusv2lem1  5336  fpwwe2  10531  fzsplit2  13446  saddisjlem  16372  smupval  16396  smueqlem  16398  prmrec  16831  ablnsg  19757  cnprest  23202  flimrest  23896  fclsrest  23937  tsmssubm  24056  setsxms  24392  tcphcph  25162  ellimc2  25803  fsumvma2  27150  chpub  27156  mdbr2  32271  mdsl2i  32297  fzsplit3  32771  posrasymb  32943  trleile  32947  fvineqsneu  37444  cnvcnvintabd  43632  grumnud  44318  mofeu  48878