HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem r19.22dva 1731
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
Hypothesis
Ref Expression
r19.22dva.1 |- ((ph /\ x e. A) -> (ps -> ch))
Assertion
Ref Expression
r19.22dva |- (ph -> (E.x e. A ps -> E.x e. A ch))
Distinct variable group:   ph,x
Proof of Theorem r19.22dva
StepHypRef Expression
1 r19.22dva.1 . . 3 |- ((ph /\ x e. A) -> (ps -> ch))
21ex 373 . 2 |- (ph -> (x e. A -> (ps -> ch)))
32r19.22dv 1729 1 |- (ph -> (E.x e. A ps -> E.x e. A ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  E.wrex 1638
This theorem is referenced by:  dffo4 3805  noinfep 4612  cnegextlem2 5318  arch 6018  bndndx 6020  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrunb1 6036  uzwo3lem1 6164  qbtwnxr 6217  qsqueeze 6218  fsequb2 6456  cau3ir 6852  cvg2 6859  caure 6864  cauim 6865  climcau 7092  caucvg 7099  cvgcmp3c 7122  reeff1o 7368  unbenlem 7447  infpnlem2 7450  infpn2 7452  bastop 7584  cnpco 7708  metcnp 7826  lmle 7895  iscms2lem3 7925  bcthlem21 7953  grpidinvlem3 7984  grpideu 7987  grpinveu 7998  isgrp2i 8011  ring2 8086  ubthlem5 8464  minveclem27 8502  minvecex 8509  htthlem12 8561  hhcms 8993  hhsscms 9067  projlem15 9116  projlem26 9127  projlem28 9129  nmopunt 9854  rnbra 9953  sumdmdi 10249  cdj3lem2b 10269
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-ral 1641  df-rex 1642
Copyright terms: Public domain