[STATEMENT]
lemma Disj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'
[PROOF STEP]
by (metis Conj_E1 Conj_E2 Disj_mono Iff_I Iff_def anti_deduction)