Theorem al2imi 1683

Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
al2imi.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
al2imi	|- ( A. x ph -> ( A. x ps -> A. x ch ) )

Proof of Theorem al2imi

Step	Hyp	Ref	Expression
1		al2im 1682	. 2 |- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )
2		al2imi.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	mpg 1667	1 |- ( A. x ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1665  ax-4 1678

This theorem is referenced by:  alanimi  1684  alimdh  1685  albi  1686  aleximi  1700  19.33b  1740  axc112  1993  axc11nlem  1994  axc10  2058  axc11nlemOLD  2103  sbequi  2169  sbi1  2186  moim  2315  2eu6  2356  ral2imi  2813  ralimOLD  2819  ceqsalt  3104  difin0ss  3861  intssOLD  4274  hbntg  30446  bj-2alim  31188  bj-axc10v  31264  bj-axc11nlemv  31301  bj-ceqsalt0  31439  bj-ceqsalt1  31440  wl-aetr  31776  wl-aleq  31781  wl-nfeqfb  31783  axc11-o  32440  pm10.57  36577  2al2imi  36579  19.41rg  36774  hbntal  36777