[STATEMENT]
lemma ent_ex_inst2: "\<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
using ent_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P \<Longrightarrow>\<^sub>A ?Q; ?Q \<Longrightarrow>\<^sub>A ?R\<rbrakk> \<Longrightarrow> ?P \<Longrightarrow>\<^sub>A ?R

goal (1 subgoal):
 1. \<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
by blast