NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  al2imi Unicode version

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

Proof of Theorem al2imi
StepHypRef Expression
1 al2imi.1 . . 3
21alimi 1559 . 2
3 alim 1558 . 2
42, 3syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1546  ax-5 1557
This theorem is referenced by:  alanimi  1562  alimdh  1563  albi  1564  exim  1575  19.33b  1608  sp  1747  spOLD  1748  hbnt  1775  nfndOLD  1792  hbimdOLD  1816  equsalhwOLD  1839  nfaldOLD  1853  dvelimv  1939  ax10lem6  1943  ax9o  1950  ax10o  1952  cbv1h  1978  sbi1  2063  sbal1  2126  ax10o-o  2203  moim  2250  ralim  2685  ceqsalt  2881  difin0ss  3616  intss  3947
  Copyright terms: Public domain W3C validator