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

Theorem al2imi 1616
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 al2imi.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21alimi 1614 . 2  |-  ( A. x ph  ->  A. x
( ps  ->  ch ) )
3 alim 1613 . 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 setvar class
Syntax hints:    -> wi 4   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1601  ax-4 1612
This theorem is referenced by:  alanimi  1617  alimdh  1618  albi  1619  aleximi  1632  eximOLD  1634  19.33b  1673  axc112  1884  axc11nlem  1885  axc10  1973  cbv1hOLD  1988  axc11nlemOLD  2021  equveliOLD  2062  sbequi  2089  sbi1  2107  sbal1OLD  2194  axc11-o  2274  moim  2341  2eu6  2393  ral2imi  2852  ralimOLD  2858  ceqsalt  3136  difin0ss  3893  intss  4303  hbntg  28831  wl-aetr  29576  wl-aleq  29581  wl-nfeqfb  29583  pm10.57  30870  2al2imi  30872  19.41rg  32412  hbntal  32415  bj-2alim  33298  bj-axc10v  33368  bj-axc11nlemv  33405  bj-ceqsalt0  33539  bj-ceqsalt1  33540
  Copyright terms: Public domain W3C validator