Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29_2a Unicode version

Theorem r19.29_2a 3001
 Description: A commonly used pattern based on r19.29 2992, version with two restricted quantifiers (Contributed by Thierry Arnoux, 26-Nov-2017.)
Hypotheses
Ref Expression
r19.29_2a.1
r19.29_2a.2
Assertion
Ref Expression
r19.29_2a
Distinct variable groups:   ,   ,,   ,,

Proof of Theorem r19.29_2a
StepHypRef Expression
1 r19.29_2a.1 . . . . . 6
21ex 434 . . . . 5
32ralrimiva 2871 . . . 4
43ralrimiva 2871 . . 3
5 r19.29_2a.2 . . 3
64, 5r19.29d2r 3000 . 2
7 pm3.35 587 . . . . 5
87ancoms 453 . . . 4
98rexlimivw 2946 . . 3
109rexlimivw 2946 . 2
116, 10syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807  E.wrex 2808 This theorem is referenced by:  trust  20732  utoptop  20737  metusttoOLD  21060  metustto  21061  restmetu  21090  tgbtwndiff  23897  legov  23972  legso  23985  tglnne  24008  tglndim0  24009  tglinethru  24016  tglnne0  24020  tglnpt2  24021  footex  24095  midex  24111  opptgdim2  24117  f1otrge  24175  archiabllem2c  27739  txomap  27837  qtophaus  27839  pstmfval  27875  eulerpartlemgvv  28315  irrapxlem4  30761 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
 Copyright terms: Public domain W3C validator