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

Theorem alimi 1385
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alimi.1 (𝜑𝜓)
Assertion
Ref Expression
alimi (∀𝑥𝜑 → ∀𝑥𝜓)

Proof of Theorem alimi
StepHypRef Expression
1 ax-5 1377 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1381 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283
This theorem was proved from axioms:  ax-mp 7  ax-5 1377  ax-gen 1379
This theorem is referenced by:  2alimi  1386  al2imi  1388  alrimih  1399  hbal  1407  19.26  1411  19.33  1414  hbequid  1447  equidqe  1466  hbim  1478  hbor  1479  nford  1500  nfand  1501  nfalt  1511  19.21ht  1514  exbi  1536  19.29  1552  19.25  1558  alexim  1577  alexnim  1580  19.9hd  1593  19.32r  1611  ax10  1646  spimh  1666  equvini  1682  nfexd  1685  stdpc4  1699  ax10oe  1719  sbcof2  1732  sb4bor  1757  nfsb2or  1759  spsbim  1765  ax16i  1780  sbi2v  1814  nfsbt  1892  nfsbd  1893  sbalyz  1917  hbsb4t  1931  dvelimor  1936  sbal2  1940  mo2n  1970  eumo0  1973  mor  1984  bm1.1  2067  alral  2410  rgen2a  2418  ralimi2  2424  rexim  2456  r19.32r  2502  ceqsalt  2626  spcgft  2676  spcegft  2678  spc2gv  2689  spc3gv  2691  rspct  2695  elabgt  2736  reu6  2782  sbciegft  2845  csbnestgf  2955  rabss2  3078  rabxmdc  3277  undif4  3307  ssdif0im  3309  inssdif0im  3312  ssundifim  3327  ralf0  3346  ralm  3347  intmin4  3666  dfiin2g  3713  invdisj  3782  trint  3892  a9evsep  3902  axnul  3905  csbexga  3908  ordunisuc2r  4260  tfi  4325  peano5  4341  ssrelrel  4460  issref  4731  iotanul  4906  iota4  4909  dffun5r  4938  fv3  5223  mptfvex  5282  ssoprab2  5586  mpt2fvex  5854  tfri1dALT  5994  bj-nfalt  10711  elabgft1  10724  bj-rspgt  10732  bj-axemptylem  10826  bj-indind  10870  setindis  10905  bdsetindis  10907  bj-inf2vnlem1  10908  bj-inf2vn  10912  bj-inf2vn2  10913
  Copyright terms: Public domain W3C validator