Theorem al2imi 1743

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

Syntax hints:   -> wi 4   A.wal 1481

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

This theorem is referenced by:  alanimi  1744  alimdh  1745  albi  1746  aleximi  1759  19.33b  1813  aevlem0  1980  axc11nlemOLD2  1988  axc16g  2134  axc11rvOLD  2140  axc11nlemOLD  2160  axc11r  2187  axc10  2252  axc11nlemALT  2306  sbequi  2375  sbi1  2392  moim  2519  2eu6  2558  ral2imi  2947  ceqsalt  3228  difin0ss  3946  hbntg  31711  bj-2alim  32594  bj-ssbim  32621  bj-axc10v  32717  bj-ceqsalt0  32873  bj-ceqsalt1  32874  wl-spae  33306  wl-aetr  33317  wl-aleq  33322  wl-nfeqfb  33323  axc11-o  34236  pm10.57  38570  2al2imi  38572  19.41rg  38766  hbntal  38769