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

Theorem reximdva 2596
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
reximdva (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 115 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2594 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2164  wrex 2473
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478
This theorem is referenced by:  reximddv  2597  reximddv2  2599  dffo4  5707  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  prarloclemarch  7480  appdivnq  7625  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemloc  7669  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  archrecpr  7726  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemladdfu  7739  caucvgprlemlim  7743  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemexbt  7768  caucvgprprlemlim  7773  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemlub  7786  archsr  7844  suplocsrlemb  7868  suplocsrlempr  7869  cnegexlem2  8197  bndndx  9242  elpq  9717  qbtwnxr  10329  expnbnd  10737  expnlbnd2  10739  caucvgre  11128  cvg1nlemres  11132  r19.29uz  11139  resqrexlemglsq  11169  resqrexlemga  11170  cau3lem  11261  qdenre  11349  2clim  11447  climcn1  11454  climcn2  11455  climsqz  11481  climsqz2  11482  climcau  11493  divcnv  11643  divalglemex  12066  dvdsbnd  12096  bezoutlemzz  12142  bezoutlemaz  12143  bezoutlembz  12144  bezoutlembi  12145  lcmgcdlem  12218  divgcdcoprmex  12243  exprmfct  12279  prmdvdsfz  12280  pclemub  12428  pc2dvds  12471  pcprmpw  12475  dvdsprmpweqle  12478  infpnlem2  12501  prmunb  12503  ennnfonelemhom  12575  ctinf  12590  sgrpidmndm  13004  grpinveu  13113  dfgrp3mlem  13173  ringadd2  13526  znunit  14158  cnpnei  14398  txlm  14458  metequiv2  14675  metrest  14685  mulc1cncf  14768  cncfco  14770  dedekindeulemlu  14800  suplociccreex  14803  dedekindicclemlu  14809  ivthinc  14822  cnplimcim  14846  cnplimclemr  14848  limccnpcntop  14854  limccoap  14857  elply2  14914  subctctexmid  15561
  Copyright terms: Public domain W3C validator