Theorem al2imi 1616

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		al2imi.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	alimi 1614	. 2 |- ( A. x ph -> A. x ( ps -> ch ) )
3		alim 1613	. 2 |- ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) )
4	2, 3	syl 16	1 |- ( A. x ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1377

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

This theorem is referenced by:  alanimi  1617  alimdh  1618  albi  1619  aleximi  1632  eximOLD  1634  19.33b  1673  axc112  1884  axc11nlem  1885  axc10  1973  cbv1hOLD  1988  axc11nlemOLD  2021  equveliOLD  2062  sbequi  2089  sbi1  2107  sbal1OLD  2194  axc11-o  2274  moim  2341  2eu6  2393  ral2imi  2852  ralimOLD  2858  ceqsalt  3136  difin0ss  3893  intss  4303  hbntg  28831  wl-aetr  29576  wl-aleq  29581  wl-nfeqfb  29583  pm10.57  30870  2al2imi  30872  19.41rg  32412  hbntal  32415  bj-2alim  33298  bj-axc10v  33368  bj-axc11nlemv  33405  bj-ceqsalt0  33539  bj-ceqsalt1  33540