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

Theorem al2imi 1548
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 1546 . 2  |-  ( A. x ph  ->  A. x
( ps  ->  ch ) )
3 alim 1545 . 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 1527
This theorem is referenced by:  alanimi  1549  alimdh  1550  albi  1551  exim  1562  19.33b  1595  sp  1716  hbimd  1721  hbnt  1724  equsalhw  1730  nfnd  1760  nfald  1775  dvelimv  1879  ax10lem6  1883  ax9o  1890  ax10o  1892  cbv1h  1918  sbi1  2003  sbal1  2065  ax10o-o  2142  moim  2189  ralim  2614  ceqsalt  2810  difin0ss  3520  intss  3883  hbntg  24162  pm10.56  27565  pm10.57  27566  2al2imi  27568  19.41rg  28316  hbntal  28319  ax10lem17ALT  29123  ax9lem3  29142  ax9lem4  29143  ax9lem9  29148  ax9lem17  29156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544
  Copyright terms: Public domain W3C validator