You could use a rewrite database, for instance:
Require Import Setoid.
Require Import Bool.
Lemma andb_prop_iff x y: Is_true (x && y) <-> Is_true x /\ Is_true y.
Proof.
split; [apply andb_prop_elim | apply andb_prop_intro].
Qed.
Lemma orb_prop_iff x y: Is_true (x || y) <-> Is_true x \/ Is_true y.
Proof.
split; [apply orb_prop_elim | apply orb_prop_intro].
Qed.
Hint Rewrite
andb_prop_iff
orb_prop_iff
: quotebool.
Goal forall a b c, Is_true (a && b || c && (b || a)).
intros.
autorewrite with quotebool.