Theorem ralimia 2166

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
ralimia.1	|- (x e. A -> (ph -> ps))

Assertion

Ref	Expression
ralimia	|- (A.x e. A ph -> A.x e. A ps)

Proof of Theorem ralimia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 |- (x e. A -> (ph -> ps))
2	1	a2i 10	. 2 |- ((x e. A -> ph) -> (x e. A -> ps))
3	2	ralimi2 2165	1 |- (A.x e. A ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  ralimiaa 2167  ralimi 2168  r19.12 2204  r19.12OLD 2205  truni 3425  exfo 4795  ixpf 5415  tz9.12lem3 5772  aceq6a 5903  kmlem12 5938  brdom6disj 5967  arch 7280  cvg2i 8174  caurei 8179  cauimi 8180  fsum1i 8265  clm4i 8340  climcmplem 8397  iserzcmp0 8403  climabslem 8408  cvgcmp3ci 8447  reccnv 8479  expcnvlem1 8488  lmfexlem3 9236  ubthlem5 9876  hlimuniii 10741  spanuni 11100  lnopunilem1 11572  truniOLD 13792  prjmapcp 14507  prjnpl 14510  prl2 14514  fprod1i 14673  intartar 15255  pwtsm 15266  subtsm 15267  indexa 15753  sstotbnd 15936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain