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

Theorem al2imi 1695
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 1694 . 2  |-  ( A. x ( ph  ->  ( ps  ->  ch )
)  ->  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) ) )
2 al2imi.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2mpg 1679 1  |-  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1677  ax-4 1690
This theorem is referenced by:  alanimi  1696  alimdh  1697  albi  1698  aleximi  1712  19.33b  1756  aevlem0  1896  axc11nlemOLD2  1902  axc11r  2040  axc11nlemOLD  2041  axc10  2109  axc11nlemALT  2156  sbequi  2224  sbi1  2241  moim  2368  2eu6  2407  ral2imi  2791  ceqsalt  3056  difin0ss  3745  hbntg  30523  bj-2alim  31266  bj-ssbim  31298  bj-axc10v  31384  bj-axc11nlemv  31413  bj-ceqsalt0  31550  bj-ceqsalt1  31551  wl-aetr  31933  wl-aleq  31938  wl-nfeqfb  31940  axc11-o  32586  pm10.57  36790  2al2imi  36792  19.41rg  36987  hbntal  36990
  Copyright terms: Public domain W3C validator