ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  alimi Structured version   GIF version

Theorem alimi 1320
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alimi.1 (φψ)
Assertion
Ref Expression
alimi (xφxψ)

Proof of Theorem alimi
StepHypRef Expression
1 ax-5 1312 . 2 (x(φψ) → (xφxψ))
2 alimi.1 . 2 (φψ)
31, 2mpg 1316 1 (xφxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224
This theorem was proved from axioms:  ax-mp 7  ax-5 1312  ax-gen 1314
This theorem is referenced by:  2alimi  1321  al2imi  1323  alrimih  1334  hbal  1342  19.26  1346  19.33  1349  hbequid  1383  equidqe  1402  hbim  1415  hbor  1416  nford  1437  nfand  1438  nfalt  1448  19.21ht  1451  exbi  1473  19.29  1489  19.25  1495  alexim  1514  alexnim  1517  19.9hd  1530  19.32r  1548  ax10  1583  spimh  1603  equvini  1619  nfexd  1622  stdpc4  1636  ax10oe  1656  sbcof2  1669  sb4bor  1694  nfsb2or  1696  spsbim  1702  ax16i  1716  sbi2v  1750  nfsbt  1828  nfsbd  1829  sbalyz  1853  hbsb4t  1867  dvelimor  1872  sbal2  1876  mo2n  1906  eumo0  1909  mor  1920  bm1.1  2003  alral  2341  rgen2a  2349  ralimi2  2355  rexim  2387  r19.32r  2431  ceqsalt  2553  spcgft  2603  spcegft  2605  spc2gv  2616  spc3gv  2618  rspct  2622  elabgt  2657  reu6  2703  sbciegft  2766  csbnestgf  2871  rabss2  2996  rabxmdc  3222  undif4  3257  ssdif0im  3259  inssdif0im  3264  ssundifim  3279  ralf0  3299  ralm  3300  intmin4  3613  dfiin2g  3660  invdisj  3729  trint  3839  a9evsep  3849  axnul  3852  csbexgOLD  3855  ordunisuc2r  4185  tfi  4228  peano5  4244  ssrelrel  4363  issref  4630  iotanul  4805  iota4  4808  fv3  5118  mptfvex  5177  ssoprab2  5480  mpt2fvex  5748  bj-nfalt  7150  elabgft1  7163  bj-rspgt  7171  peano5set  7301  setindis  7324  bdsetindis  7326  bj-inf2vnlem1  7327  bj-inf2vn  7331  bj-inf2vn2  7332
  Copyright terms: Public domain W3C validator