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  1641  reusv1  5366  reusv2lem1  5367  fpwwe2  10656  fzsplit2  13608  saddisjlem  16560  smupval  16584  smueqlem  16586  prmrec  17020  ablnsg  19980  cnprest  23520  flimrest  24215  fclsrest  24256  tsmssubm  24375  setsxms  24711  tcphcph  25471  ellimc2  26111  fsumvma2  27458  chpub  27464  mdbr2  32785  mdsl2i  32811  fzsplit3  33272  posrasymb  33415  trleile  33419  fvineqsneu  38173  cnvcnvintabd  44448  grumnud  45118  mofeu  49784  n0als  50753