Theorem reximdv 3182

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3178	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  r19.12  3316  ss2rexv  4010  reusv3  5378  fvelima  6950  iunpw  7772  frxp  8124  nnaordex2  8627  ssfiALT  9161  ordtypelem2  9484  wdom2d  9545  xpwdomg  9550  cff1  10253  iunfo  10534  nqereu  10925  reclem3pr  11045  map2psrpr  11106  supsrlem  11107  1re  11219  elss2prb  14538  exprelprel  14540  o1lo1  15607  rlimcn1  15658  subcn2  15665  lo1add  15697  lo1mul  15698  pythagtriplem19  16910  vdwnnlem2  17073  ramub2  17091  sylow2alem2  19711  lsmless2x  19738  efgrelexlemb  19843  scmateALT  22698  decpmatmulsumfsupp  22959  pmatcollpw1lem1  22960  pmatcollpw2lem  22963  pm2mpmhmlem1  23004  cpmidpmatlem3  23058  cpmidgsum2  23065  tgcl  23155  neiss  23295  ssnei2  23302  tgcnp  23439  cnpco  23453  cnpresti  23474  lmcnp  23490  hausnei2  23539  1stcrest  23639  nlly2i  23662  llyss  23665  nllyss  23666  reftr  23700  lfinun  23711  txcnpi  23794  txcmplem1  23827  tx1stc  23836  nrmr0reg  23935  fbssfi  24023  fbfinnfr  24027  fgcl  24064  ufinffr  24115  elfm2  24134  fmfnfmlem1  24140  fmco  24147  fbflim2  24163  flffbas  24181  flftg  24182  cnpflf2  24186  alexsubALT  24237  cnextcn  24253  isucn2  24464  ucnima  24466  blssexps  24612  blssex  24613  mopni3  24680  neibl  24687  metss  24694  metcnp3  24726  cfilucfil  24745  metustbl  24752  psmetutop  24753  mpomulcn  25055  rescncf  25085  lebnum  25152  xlebnum  25153  lebnumii  25154  lmmbr  25446  fgcfil  25459  ovolsslem  25672  ovolunlem1  25685  ovoliunnul  25695  itgcn  26033  ellimc3  26067  c1lip3  26187  itgsubstlem  26236  plyss  26385  ulmclm  26579  ulmcau  26587  ulmcn  26591  rlimcxp  27167  chtppilimlem2  27667  chtppilim  27668  madess  28088  lrrecfr  28165  midex  29047  umgrnloop0  29488  usgrnloop0ALT  29584  uhgr2edg  29587  vtxduhgr0nedg  29871  wlkonl1iedg  30042  elwspths2on  30340  elwspths2onw  30341  3cyclfrgrrn2  30667  isgrpo  30878  tpr2rico  34325  esumpcvgval  34491  omssubadd  34714  r1filim  35515  fineqvnttrclse  35553  vonf1oonfo  35615  connpconn  35740  cvmliftlem15  35803  cvmlift2lem10  35817  satfdmlem  35873  fmla1  35892  satffunlem1lem2  35908  satffunlem2lem2  35911  fnessref  36901  ttctr  37037  fvineqsneq  38091  pibt2  38096  ptrecube  38304  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  fdc1  38430  sstotbnd3  38460  totbndss  38461  heibor1lem  38493  heibor1  38494  opidonOLD  38536  rngmgmbs4  38615  lvoli2  40388  paddss2  40625  lhpexle1lem  40814  lhpexle2lem  40816  dvhdimlem  42251  dvh3dim3N  42256  mapdh9a  42596  hdmap11lem2  42649  fiphp3d  43579  pell1qrss14  43628  minregex  44293  mnuop3d  45014  grumnudlem  45028  ismnushort  45044  eliuniin  45850  restuni3  45869  eliuniin2  45871  disjrnmpt2  45939  rnmptbd2lem  45996  ssfiunibd  46061  supminfxrrnmpt  46218  climrec  46352  islptre  46368  lptre2pt  46387  limsupmnfuzlem  46473  limsupre3lem  46479  limsupvaluz2  46485  supcnvlimsup  46487  liminfvalxr  46530  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  stoweidlem27  46774  stoweidlem29  46776  stoweidlem35  46782  stoweidlem48  46795  stoweidlem62  46809  fourierdlem48  46901  fourierdlem64  46917  fourierdlem65  46918  fourierdlem71  46924  fourierdlem73  46926  fourierdlem94  46947  fourierdlem103  46956  fourierdlem104  46957  fourierdlem112  46965  fourierdlem113  46966  sge0isum  47174  sge0seq  47193  meaiuninclem  47227  carageniuncllem2  47269  ovnsslelem  47307  hoidmvlelem1  47342  2reuimp  47885  afvelima  47937  sgoldbeven3prm  48581  nnsum4primes4  48587  nnsum4primesprm  48589  nnsum4primesgbe  48591  nnsum4primesle9  48593  grtriprop  48739  pgrpgt2nabl  49179  opnneilv  49720  sepnsepo  49735