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

Theorem alimi 1431
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 1423 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1427 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-5 1423  ax-gen 1425
This theorem is referenced by:  2alimi  1432  al2imi  1434  alrimih  1445  hbal  1453  19.26  1457  19.33  1460  hbequid  1493  equidqe  1512  hbim  1524  hbor  1525  nford  1546  nfand  1547  nfalt  1557  19.21ht  1560  exbi  1583  19.29  1599  19.25  1605  alexim  1624  alexnim  1627  19.9hd  1640  19.32r  1658  ax10  1695  spimh  1715  equvini  1731  nfexd  1734  stdpc4  1748  ax10oe  1769  sbcof2  1782  sb4bor  1807  nfsb2or  1809  spsbim  1815  ax16i  1830  sbi2v  1864  nfsbt  1947  nfsbd  1948  sbalyz  1972  hbsb4t  1986  dvelimor  1991  sbal2  1995  mo2n  2025  eumo0  2028  mor  2039  bm1.1  2122  alral  2476  rgen2a  2484  ralimi2  2490  rexim  2524  r19.32r  2576  ceqsalt  2707  spcgft  2758  spcegft  2760  spc2gv  2771  spc3gv  2773  rspct  2777  elabgt  2820  reu6  2868  sbciegft  2934  csbeq2  3021  csbnestgf  3047  ssrmof  3155  rabss2  3175  rabxmdc  3389  undif4  3420  ssdif0im  3422  inssdif0im  3425  ssundifim  3441  ralf0  3461  ralm  3462  intmin4  3794  dfiin2g  3841  invdisj  3918  trint  4036  a9evsep  4045  axnul  4048  csbexga  4051  exmidn0m  4119  exmidsssn  4120  exmidsssnc  4121  exmid0el  4122  ordunisuc2r  4425  tfi  4491  peano5  4507  ssrelrel  4634  issref  4916  iotanul  5098  iota4  5101  dffun5r  5130  fv3  5437  mptfvex  5499  ssoprab2  5820  mpofvex  6094  tfri1dALT  6241  prodeq2w  11318  bj-nfalt  12960  elabgft1  12974  bj-rspgt  12982  bj-axemptylem  13079  bj-indind  13119  setindis  13154  bdsetindis  13156  bj-inf2vnlem1  13157  bj-inf2vn  13161  bj-inf2vn2  13162
  Copyright terms: Public domain W3C validator