MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  al2imi Structured version   Visualization version   Unicode version

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
StepHypRef 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 ) )
31, 2mpg 1671 1  |-  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator