Theorem al2imi 1687

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 1686	. 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 1671	1 |- ( A. x ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1442

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

This theorem is referenced by:  alanimi  1688  alimdh  1689  albi  1690  aleximi  1704  19.33b  1748  axc112  2020  axc11nlem  2021  axc10  2096  axc11nlemALT  2142  sbequi  2204  sbi1  2221  moim  2348  2eu6  2387  ral2imi  2776  ralimOLD  2782  ceqsalt  3070  difin0ss  3833  intssOLD  4256  hbntg  30452  bj-2alim  31202  bj-ssbim  31234  bj-axc10v  31318  bj-axc11nlemv  31347  bj-ceqsalt0  31482  bj-ceqsalt1  31483  wl-aetr  31863  wl-aleq  31868  wl-nfeqfb  31870  axc11-o  32522  pm10.57  36720  2al2imi  36722  19.41rg  36917  hbntal  36920