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

Theorem alimi 1360
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 1352 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1356 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1257
This theorem was proved from axioms:  ax-mp 7  ax-5 1352  ax-gen 1354
This theorem is referenced by:  2alimi  1361  al2imi  1363  alrimih  1374  hbal  1382  19.26  1386  19.33  1389  hbequid  1422  equidqe  1441  hbim  1453  hbor  1454  nford  1475  nfand  1476  nfalt  1486  19.21ht  1489  exbi  1511  19.29  1527  19.25  1533  alexim  1552  alexnim  1555  19.9hd  1568  19.32r  1586  ax10  1621  spimh  1641  equvini  1657  nfexd  1660  stdpc4  1674  ax10oe  1694  sbcof2  1707  sb4bor  1732  nfsb2or  1734  spsbim  1740  ax16i  1754  sbi2v  1788  nfsbt  1866  nfsbd  1867  sbalyz  1891  hbsb4t  1905  dvelimor  1910  sbal2  1914  mo2n  1944  eumo0  1947  mor  1958  bm1.1  2041  alral  2384  rgen2a  2392  ralimi2  2398  rexim  2430  r19.32r  2474  ceqsalt  2597  spcgft  2647  spcegft  2649  spc2gv  2660  spc3gv  2662  rspct  2666  elabgt  2707  reu6  2753  sbciegft  2816  csbnestgf  2926  rabss2  3051  rabxmdc  3277  undif4  3312  ssdif0im  3314  inssdif0im  3319  ssundifim  3334  ralf0  3352  ralm  3353  intmin4  3671  dfiin2g  3718  invdisj  3787  trint  3897  a9evsep  3907  axnul  3910  csbexga  3913  ordunisuc2r  4268  tfi  4333  peano5  4349  ssrelrel  4468  issref  4735  iotanul  4910  iota4  4913  dffun5r  4942  fv3  5225  mptfvex  5284  ssoprab2  5589  mpt2fvex  5857  bj-nfalt  10291  elabgft1  10304  bj-rspgt  10312  bj-axemptylem  10399  bj-indind  10443  peano5setOLD  10452  setindis  10479  bdsetindis  10481  bj-inf2vnlem1  10482  bj-inf2vn  10486  bj-inf2vn2  10487
  Copyright terms: Public domain W3C validator