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  1031  cador  1610  reusv1  5334  reusv2lem1  5335  fpwwe2  10557  fzsplit2  13494  saddisjlem  16424  smupval  16448  smueqlem  16450  prmrec  16884  ablnsg  19813  cnprest  23264  flimrest  23958  fclsrest  23999  tsmssubm  24118  setsxms  24454  tcphcph  25214  ellimc2  25854  fsumvma2  27191  chpub  27197  mdbr2  32382  mdsl2i  32408  fzsplit3  32881  posrasymb  33042  trleile  33046  fvineqsneu  37741  cnvcnvintabd  44045  grumnud  44731  mofeu  49335