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

Theorem al2imi 1551
Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 5-Aug-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 al2imi.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21alimi 1549 . 2  |-  ( A. x ph  ->  A. x
( ps  ->  ch ) )
3 alim 1548 . 2  |-  ( A. x ( ps  ->  ch )  ->  ( A. x ps  ->  A. x ch ) )
42, 3syl 15 1  |-  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  alanimi  1552  alimdh  1553  albi  1554  exim  1565  19.33b  1598  sp  1728  hbimd  1733  hbnt  1736  equsalhw  1742  nfnd  1772  nfald  1787  dvelimv  1892  ax10lem6  1896  ax9o  1903  ax10o  1905  cbv1h  1931  sbi1  2016  sbal1  2078  ax10o-o  2155  moim  2202  ralim  2627  ceqsalt  2823  difin0ss  3533  intss  3899  hbntg  24233  pm10.56  27668  pm10.57  27669  2al2imi  27671  19.41rg  28615  hbntal  28618  nfaldwAUX7  29429  dvelimvNEW7  29439  ax9oNEW7  29446  ax10oNEW7  29453  cbv1hwAUX7  29488  sbi1NEW7  29538  sbal1NEW7  29587  nfaldOLD7  29644  cbv1hOLD7  29673  ax10lem17ALT  29745  ax9lem3  29764  ax9lem4  29765  ax9lem9  29770  ax9lem17  29778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1536  ax-5 1547
  Copyright terms: Public domain W3C validator