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

Theorem alimi 1317
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 1309 . 2 (x(φψ) → (xφxψ))
2 alimi.1 . 2 (φψ)
31, 2mpg 1313 1 (xφxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1221
This theorem was proved from axioms:  ax-mp 7  ax-5 1309  ax-gen 1311
This theorem is referenced by:  2alimi  1318  al2imi  1320  alrimih  1331  hbal  1339  19.26  1343  19.33  1346  hbequid  1379  equidqe  1398  hbim  1410  hbor  1411  nford  1432  nfand  1433  nfalt  1443  19.21ht  1446  exbi  1468  19.29  1484  19.25  1490  alexim  1509  alexnim  1512  19.9hd  1525  19.32r  1543  ax10  1578  spimh  1598  equvini  1614  nfexd  1617  stdpc4  1631  ax10oe  1651  sbcof2  1664  sb4bor  1689  nfsb2or  1691  spsbim  1697  ax16i  1711  sbi2v  1745  nfsbt  1823  nfsbd  1824  sbalyz  1848  hbsb4t  1862  dvelimor  1867  sbal2  1871  mo2n  1901  eumo0  1904  mor  1915  bm1.1  1998  alral  2336  rgen2a  2344  ralimi2  2350  rexim  2382  r19.32r  2426  ceqsalt  2548  spcgft  2598  spcegft  2600  spc2gv  2611  spc3gv  2613  rspct  2617  elabgt  2652  reu6  2698  sbciegft  2761  csbnestgf  2866  rabss2  2991  rabxmdc  3217  undif4  3252  ssdif0im  3254  inssdif0im  3259  ssundifim  3274  ralf0  3292  ralm  3293  intmin4  3606  dfiin2g  3653  invdisj  3722  trint  3832  a9evsep  3842  axnul  3845  csbexga  3848  ordunisuc2r  4177  tfi  4220  peano5  4236  ssrelrel  4355  issref  4622  iotanul  4797  iota4  4800  fv3  5110  mptfvex  5169  ssoprab2  5472  mpt2fvex  5740  bj-nfalt  8169  elabgft1  8182  bj-rspgt  8190  peano5set  8324  setindis  8347  bdsetindis  8349  bj-inf2vnlem1  8350  bj-inf2vn  8354  bj-inf2vn2  8355
  Copyright terms: Public domain W3C validator