Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem r19.20si 1698

Description: Inference quantifying both antecedent and consequent, with strong hypothesis.

Hypothesis

Ref	Expression
r19.20si.1

Assertion

Ref	Expression
r19.20si

---

Proof of Theorem r19.20si

Step	Hyp	Ref	Expression
1		r19.20si.1	. . 3
2	1	a1i 8	. 2
3	2	r19.20i 1696	1

Colors of variables: wff set class

Syntax hints:   wi 3   wcel 955  wral 1637

This theorem is referenced by:  r19.20sii 1699  reu6 1922  uniss2 2519  iunss2 2585  tfis 3117  find 3145  dffun7 3526  fununi 3549  fun11uni 3551  zfrep6 3600  fnopabg 3601  elrnopabg 3785  dffo5 3806  fopab2 3808  elrnoprabg 4108  unifi2 4533  iunfi 4543  rankonid 4667  aceq5 4712  ac5b 4725  ac6lem 4726  ac6 4727  kmlem6 4742  kmlem8 4744  kmlem13 4749  xrsupexmnf 6021  xrinfmexpnf 6022  cau3ir 6852  cau3 6853  cvganz 6861  2sumeq2dv 6932  fsum1s 6947  fsump1s 6951  fsumadd 6960  csbfsum 6965  fsummulc1 6971  fsumcmp 6978  fsumcmp0 6979  fsumcmpndx2 6980  fsumabs 6981  fsumabs2mul 6982  serzmulc1 6995  clm3 7017  clmi2 7025  clm0i 7027  climunii 7035  2climnn 7039  2climnn0 7040  climge0 7049  iserzmulc1 7072  climcmplem 7073  climsqueeze 7076  climsqueeze2 7077  iserzcmp 7078  caucvg3 7103  iserzgt0 7146  basgen2t 7581  bastop 7584  neips 7668  cncnp 7717  meteq0 7751  mettri2 7752  mettri4 7753  lmcvg2 7871  caun0 7880  xplm 7909  iscms2 7928  isgrp 7975  grpidinv 7986  grpideu 7987  grpidinv2 7994  ringdi 8083  ringdir 8084  ringass 8085  vcid 8107  vcdi 8108  vcdir 8109  vcass 8110  nvs 8229  nvz 8236  nvtri 8237  ajmoi 8450  axgroth3 8718  grothinf 8720  projlem22 9123  adjmo 9675  adjvalvalt 9777  lnopcon 9878  lnfncon 9905  cnlnssadj 9928  stge0t 10061  stle1t 10062  mdbr3 10134  mdbr4 10135  mdsl1 10156  dmdbr6at 10256  imonclem 10583

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-ral 1641

Copyright terms: Public domain