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

Theorem al2imi 1636
Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
al2imi.1
Assertion
Ref Expression
al2imi

Proof of Theorem al2imi
StepHypRef Expression
1 al2im 1635 . 2
2 al2imi.1 . 2
31, 2mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  alanimi  1637  alimdh  1638  albi  1639  aleximi  1653  eximOLD  1655  19.33b  1696  axc112  1937  axc11nlem  1938  axc10  2004  axc11nlemOLD  2048  equveliOLD  2089  sbequi  2116  sbi1  2133  axc11-o  2281  moim  2339  2eu6  2383  ral2imi  2845  ralimOLD  2851  ceqsalt  3132  difin0ss  3894  intssOLD  4308  hbntg  29238  wl-aetr  29983  wl-aleq  29988  wl-nfeqfb  29990  pm10.57  31276  2al2imi  31278  19.41rg  33323  hbntal  33326  bj-2alim  34202  bj-axc10v  34277  bj-axc11nlemv  34315  bj-ceqsalt0  34449  bj-ceqsalt1  34450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1618  ax-4 1631
  Copyright terms: Public domain W3C validator