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

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