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

Theorem reximi 2574
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
Hypothesis
Ref Expression
reximi.1 (𝜑𝜓)
Assertion
Ref Expression
reximi (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)

Proof of Theorem reximi
StepHypRef Expression
1 reximi.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝑥𝐴 → (𝜑𝜓))
32reximia 2572 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wrex 2456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-ral 2460  df-rex 2461
This theorem is referenced by:  r19.29d2r  2621  r19.35-1  2627  r19.40  2631  reu3  2929  ssiun  3930  iinss  3940  elunirn  5769  tfrcllemssrecs  6355  nnawordex  6532  iinerm  6609  erovlem  6629  xpf1o  6846  fidcenumlemim  6953  omniwomnimkv  7167  genprndl  7522  genprndu  7523  appdiv0nq  7565  ltexprlemm  7601  recexsrlem  7775  rereceu  7890  recexre  8537  aprcl  8605  rexanre  11231  climi2  11298  climi0  11299  climcaucn  11361  prodmodclem2  11587  prodmodc  11588  gcdsupex  11960  gcdsupcl  11961  bezoutlemeu  12010  dfgcd3  12013  isnsgrp  12817  eltg2b  13639  lmcvg  13802  cnptoprest  13824  lmtopcnp  13835  txbas  13843  metrest  14091  2sqlem7  14553  bj-charfunbi  14648  bj-findis  14816
  Copyright terms: Public domain W3C validator