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

Theorem alimi 1416
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 1408 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1412 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-5 1408  ax-gen 1410
This theorem is referenced by:  2alimi  1417  al2imi  1419  alrimih  1430  hbal  1438  19.26  1442  19.33  1445  hbequid  1478  equidqe  1497  hbim  1509  hbor  1510  nford  1531  nfand  1532  nfalt  1542  19.21ht  1545  exbi  1568  19.29  1584  19.25  1590  alexim  1609  alexnim  1612  19.9hd  1625  19.32r  1643  ax10  1680  spimh  1700  equvini  1716  nfexd  1719  stdpc4  1733  ax10oe  1753  sbcof2  1766  sb4bor  1791  nfsb2or  1793  spsbim  1799  ax16i  1814  sbi2v  1848  nfsbt  1927  nfsbd  1928  sbalyz  1952  hbsb4t  1966  dvelimor  1971  sbal2  1975  mo2n  2005  eumo0  2008  mor  2019  bm1.1  2102  alral  2455  rgen2a  2463  ralimi2  2469  rexim  2503  r19.32r  2555  ceqsalt  2686  spcgft  2737  spcegft  2739  spc2gv  2750  spc3gv  2752  rspct  2756  elabgt  2799  reu6  2846  sbciegft  2911  csbnestgf  3022  ssrmof  3130  rabss2  3150  rabxmdc  3364  undif4  3395  ssdif0im  3397  inssdif0im  3400  ssundifim  3416  ralf0  3436  ralm  3437  intmin4  3769  dfiin2g  3816  invdisj  3893  trint  4011  a9evsep  4020  axnul  4023  csbexga  4026  exmidn0m  4094  exmidsssn  4095  exmidsssnc  4096  exmid0el  4097  ordunisuc2r  4400  tfi  4466  peano5  4482  ssrelrel  4609  issref  4891  iotanul  5073  iota4  5076  dffun5r  5105  fv3  5412  mptfvex  5474  ssoprab2  5795  mpofvex  6069  tfri1dALT  6216  bj-nfalt  12898  elabgft1  12912  bj-rspgt  12920  bj-axemptylem  13017  bj-indind  13057  setindis  13092  bdsetindis  13094  bj-inf2vnlem1  13095  bj-inf2vn  13099  bj-inf2vn2  13100
  Copyright terms: Public domain W3C validator