Theorem reximdv 3177

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 3173	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086

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 3087

This theorem is used by:  r19.12  3311  ss2rexv  4003  reusv3  5370  fvelima  6943  iunpw  7770  frxp  8124  nnaordex2  8627  ssfiALT  9168  ordtypelem2  9491  wdom2d  9552  xpwdomg  9557  cff1  10260  iunfo  10547  nqereu  10938  reclem3pr  11058  map2psrpr  11119  supsrlem  11120  1re  11232  elss2prb  14553  exprelprel  14555  o1lo1  15624  rlimcn1  15675  subcn2  15682  lo1add  15714  lo1mul  15715  pythagtriplem19  16925  vdwnnlem2  17088  ramub2  17106  mgmidpfod  18770  sylow2alem2  19745  lsmless2x  19772  efgrelexlemb  19877  scmateALT  22734  decpmatmulsumfsupp  22998  pmatcollpw1lem1  22999  pmatcollpw2lem  23002  pm2mpmhmlem1  23043  cpmidpmatlem3  23097  cpmidgsum2  23104  tgcl  23194  neiss  23334  ssnei2  23341  tgcnp  23478  cnpco  23492  cnpresti  23513  lmcnp  23529  hausnei2  23578  1stcrest  23678  nlly2i  23702  llyss  23705  nllyss  23706  reftr  23740  lfinun  23751  txcnpi  23834  txcmplem1  23867  tx1stc  23876  nrmr0reg  23975  fbssfi  24063  fbfinnfr  24067  fgcl  24104  ufinffr  24155  elfm2  24174  fmfnfmlem1  24180  fmco  24187  fbflim2  24203  flffbas  24221  flftg  24222  cnpflf2  24226  alexsubALT  24277  cnextcn  24293  isucn2  24504  ucnima  24506  blssexps  24652  blssex  24653  mopni3  24720  neibl  24727  metss  24734  metcnp3  24766  cfilucfil  24785  metustbl  24792  psmetutop  24793  mpomulcn  25095  rescncf  25125  lebnum  25192  xlebnum  25193  lebnumii  25194  lmmbr  25486  fgcfil  25499  ovolsslem  25712  ovolunlem1  25725  ovoliunnul  25735  itgcn  26072  ellimc3  26106  c1lip3  26226  itgsubstlem  26275  plyss  26424  ulmclm  26623  ulmcau  26631  ulmcn  26635  rlimcxp  27210  chtppilimlem2  27710  chtppilim  27711  madess  28131  lrrecfr  28208  midex  29092  umgrnloop0  29566  usgrnloop0ALT  29665  uhgr2edg  29668  vtxduhgr0nedg  29952  wlkonl1iedg  30123  elwspths2on  30430  elwspths2onw  30431  3cyclfrgrrn2  30767  isgrpo  30978  tpr2rico  34422  esumpcvgval  34588  omssubadd  34811  r1filim  35612  fineqvnttrclse  35650  vonf1oonfo  35712  connpconn  35814  cvmliftlem15  35877  cvmlift2lem10  35891  satfdmlem  35947  fmla1  35966  satffunlem1lem2  35982  satffunlem2lem2  35985  fnessref  36976  ttctr  37112  fvineqsneq  38166  pibt2  38171  ptrecube  38369  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  fdc1  38496  sstotbnd3  38526  totbndss  38527  heibor1lem  38559  heibor1  38560  opidonOLD  38602  rngmgmbs4  38681  lvoli2  40454  paddss2  40691  lhpexle1lem  40880  lhpexle2lem  40882  dvhdimlem  42317  dvh3dim3N  42322  mapdh9a  42662  hdmap11lem2  42715  fiphp3d  43660  pell1qrss14  43709  minregex  44374  mnuop3d  45095  grumnudlem  45109  ismnushort  45125  eliuniin  45931  restuni3  45950  eliuniin2  45952  disjrnmpt2  46020  rnmptbd2lem  46077  ssfiunibd  46142  supminfxrrnmpt  46299  climrec  46433  islptre  46449  lptre2pt  46468  limsupmnfuzlem  46554  limsupre3lem  46560  limsupvaluz2  46566  supcnvlimsup  46568  liminfvalxr  46611  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem27  46855  stoweidlem29  46857  stoweidlem35  46863  stoweidlem48  46876  stoweidlem62  46890  fourierdlem48  46982  fourierdlem64  46998  fourierdlem65  46999  fourierdlem71  47005  fourierdlem73  47007  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem113  47047  sge0isum  47255  sge0seq  47274  meaiuninclem  47308  carageniuncllem2  47350  ovnsslelem  47388  hoidmvlelem1  47423  2reuimp  48003  afvelima  48055  sgoldbeven3prm  48699  nnsum4primes4  48705  nnsum4primesprm  48707  nnsum4primesgbe  48709  nnsum4primesle9  48711  grtriprop  48857  pgrpgt2nabl  49296  opnneilv  49835  sepnsepo  49850