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

Theorem alimi 1387
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alimi  |-  ( A. x ph  ->  A. x ps )

Proof of Theorem alimi
StepHypRef Expression
1 ax-5 1379 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1383 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285
This theorem was proved from axioms:  ax-mp 7  ax-5 1379  ax-gen 1381
This theorem is referenced by:  2alimi  1388  al2imi  1390  alrimih  1401  hbal  1409  19.26  1413  19.33  1416  hbequid  1449  equidqe  1468  hbim  1480  hbor  1481  nford  1502  nfand  1503  nfalt  1513  19.21ht  1516  exbi  1538  19.29  1554  19.25  1560  alexim  1579  alexnim  1582  19.9hd  1595  19.32r  1613  ax10  1649  spimh  1669  equvini  1685  nfexd  1688  stdpc4  1702  ax10oe  1722  sbcof2  1735  sb4bor  1760  nfsb2or  1762  spsbim  1768  ax16i  1783  sbi2v  1817  nfsbt  1895  nfsbd  1896  sbalyz  1920  hbsb4t  1934  dvelimor  1939  sbal2  1943  mo2n  1973  eumo0  1976  mor  1987  bm1.1  2070  alral  2417  rgen2a  2425  ralimi2  2431  rexim  2463  r19.32r  2510  ceqsalt  2639  spcgft  2689  spcegft  2691  spc2gv  2702  spc3gv  2704  rspct  2708  elabgt  2748  reu6  2795  sbciegft  2858  csbnestgf  2969  rabss2  3093  rabxmdc  3303  undif4  3333  ssdif0im  3335  inssdif0im  3338  ssundifim  3353  ralf0  3372  ralm  3373  intmin4  3701  dfiin2g  3748  invdisj  3817  trint  3928  a9evsep  3938  axnul  3941  csbexga  3944  exmid0el  4009  ordunisuc2r  4306  tfi  4372  peano5  4388  ssrelrel  4508  issref  4783  iotanul  4963  iota4  4966  dffun5r  4995  fv3  5293  mptfvex  5353  ssoprab2  5664  mpt2fvex  5932  tfri1dALT  6072  bj-nfalt  11134  elabgft1  11147  bj-rspgt  11155  bj-axemptylem  11252  bj-indind  11296  setindis  11331  bdsetindis  11333  bj-inf2vnlem1  11334  bj-inf2vn  11338  bj-inf2vn2  11339
  Copyright terms: Public domain W3C validator