Theorem rbaib 548

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.75  1046  cador  1640  reusv1  5358  reusv2lem1  5359  fpwwe2  10732  fzsplit2  13687  saddisjlem  16640  smupval  16664  smueqlem  16666  prmrec  17106  ablnsg  20067  cnprest  23613  flimrest  24308  fclsrest  24349  tsmssubm  24468  setsxms  24804  tcphcph  25564  ellimc2  26203  fsumvma2  27547  chpub  27553  mdbr2  32904  mdsl2i  32930  fzsplit3  33432  posrasymb  33575  trleile  33579  fvineqsneu  38428  cnvcnvintabd  44694  grumnud  45364  mofeu  50053  n0als  51081