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

Theorem al2imi 1570
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 1568 . 2  |-  ( A. x ph  ->  A. x
( ps  ->  ch ) )
3 alim 1567 . 2  |-  ( A. x ( ps  ->  ch )  ->  ( A. x ps  ->  A. x ch ) )
42, 3syl 16 1  |-  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  alanimi  1571  alimdh  1572  albi  1573  exim  1584  19.33b  1618  spOLD  1764  hbntOLD  1800  nfndOLD  1810  hbimdOLD  1835  equsalhwOLD  1861  nfaldOLD  1872  ax9o  1954  cbv1hOLD  1975  ax10lem2  2023  ax10o2  2024  dvelimvOLD  2028  ax10oOLD  2039  equveli  2085  sbi1  2132  sbal1  2203  ax10o-o  2280  moim  2327  ralim  2777  ceqsalt  2978  difin0ss  3694  intss  4071  hbntg  25433  wl-aleq  26235  pm10.56  27542  pm10.57  27543  2al2imi  27545  19.41rg  28637  hbntal  28640  nfaldwAUX7  29452  dvelimvNEW7  29462  ax9oNEW7  29469  ax10oNEW7  29476  cbv1hwAUX7  29511  sbi1NEW7  29563  sbal1NEW7  29615  nfaldOLD7  29690  cbv1hOLD7  29719
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1555  ax-5 1566
  Copyright terms: Public domain W3C validator