New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  al2imi GIF 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 (xφ → (xψxχ))

Proof of Theorem al2imi
StepHypRef Expression
1 al2imi.1 . . 3 (φ → (ψχ))
21alimi 1559 . 2 (xφx(ψχ))
3 alim 1558 . 2 (x(ψχ) → (xψxχ))
42, 3syl 15 1 (xφ → (xψxχ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  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