Theorem rbaib 906

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 905	. 2
3	2	bicomd 201	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  cador  1458  reusv1  4652  reusv2lem1  4653  opres  5288  cores  5515  fvres  5885  fpwwe2  9042  fzsplit2  11739  saddisjlem  14114  smupval  14138  smueqlem  14140  prmrec  14440  ablnsg  16853  cnprest  19790  flimrest  20484  fclsrest  20525  tsmssubm  20644  setsxms  20982  tchcph  21680  ellimc2  22281  fsumvma2  23489  chpub  23495  mdbr2  27215  mdsl2i  27241  fzsplit3  27599  posrasymb  27645  trleile  27654

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 185  df-an 371