Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem 19.20i 990

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
19.20i.1

Assertion

Ref	Expression
19.20i

---

Proof of Theorem 19.20i

Step	Hyp	Ref	Expression
1		19.20i.1	. . 3
2	1	a4s 982	. 2
3	2	a5i 987	1

Colors of variables: wff set class

Syntax hints:   wi 3  wal 952

This theorem is referenced by:  19.20i2 991  19.20 992  19.20ii 993  19.21ai 996  hbal 1003  ax67 1018  ax67to6 1019  ax67to7 1020  ax467 1021  ax467to6 1023  ax467to7 1024  19.9d 1035  19.18 1048  19.26 1065  19.25 1082  19.33 1089  19.33b 1090  hbimd 1108  19.21t 1113  equid 1124  ax10 1139  a4im 1157  stdpc4 1183  sbied 1193  aev 1206  ax11 1217  hbsb4 1246  sbco3 1255  sbcom 1256  sb9i 1261  ax16i 1268  sbal1 1344  sbal2 1356  ax11eq 1361  ax11el 1362  ax11indi 1365  a12stdy3 1372  a12study 1376  mo 1391  eumo0 1393  mo2 1398  2mo 1445  bm1.1 1460  alral 1689  rgen2a 1696  r19.20i2 1700  r19.27av 1751  ceqsalg 1821  elabgt 1891  reu3 1927  sbciegft 1955  csbexg 2004  csbiegft 2025  csbnestg 2032  sbcnestg 2034  rabss2 2125  unss1 2195  ssrin 2230  undif4 2321  ralf0 2355  intmin4 2554  iinss 2595  axrep1 2689  axrep2 2690  bm1.3ii 2701  axnul 2704  axpr 2773  ssrel 3242  asymref2 3432  funin 3558  zfrep6 3606  fv3 3724  tfrlem5 3906  dfom3 4610  aceq5 4720  aceq6a 4721  aceq6b 4722  kmlem1 4745  kmlem13 4757  zorn 4777  brdom3 4781  brdom4 4783  axpowndlem2 4930  axacndlem1 4939  axacndlem2 4940  axacndlem3 4941  axacndlem4 4942  axacnd 4944  suppsr2 5203  suppsr3 5204  pre-axsup 5271  peano2nn 5891  islp2 7697  chsscm 9051  chcmh 9052  pjnormss 10034

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

Copyright terms: Public domain