Theorem alimi 1338

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
alimi.1	|- (ph -> ps)

Assertion

Ref	Expression
alimi	|- (A.xph -> A.xps)

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		alimi.1	. . 3 |- (ph -> ps)
2	1	a4s 1330	. 2 |- (A.xph -> ps)
3	2	a5i 1335	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  2alimi 1339  alim 1340  al2imi 1341  19.21ai 1345  hbal 1352  ax67 1367  ax67to6 1368  ax67to7 1369  ax467 1370  ax467to6 1372  ax467to7 1373  19.9d 1384  exbi 1397  19.26 1416  19.29 1421  19.25 1435  19.33 1443  19.33b 1444  19.33bOLD 1445  hbimd 1468  19.21t 1473  equid 1484  ax10 1501  a4im 1520  equvini 1531  stdpc4 1550  sbiedOLD 1564  aevOLD 1578  ax11 1589  hbsb4 1620  hbsb4t 1621  sbco3 1631  sbcom 1632  sb9i 1640  ax16i 1647  sbal1 1737  sbal2 1749  ax11eq 1754  ax11el 1755  ax11indi 1758  a12stdy3 1765  a12study 1769  mo 1787  eumo0 1790  mo2 1795  2mo 1851  bm1.1 1870  alral 2153  rgen2a 2160  rgen2aOLD 2161  ralimi2 2165  r19.27avOLD 2225  ceqsalgOLD 2315  elabgt 2400  elabgtOLD 2401  euind 2439  reu6 2443  reuind 2450  sbciegft 2482  csbexg 2548  csbiegft 2573  csbnestg 2581  sbcnestg 2583  rabss2 2689  rabss2OLD 2690  unss1OLD 2774  ssrinOLD 2818  undif4 2930  undif4OLD 2931  ralf0 2975  intmin4 3246  dfiin2g 3286  iinssOLD 3305  trint 3426  axrep1 3429  axrep2 3430  bm1.3ii 3441  axnul 3444  axpr 3523  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  asymref2 4310  asymref2OLD 4311  funinOLD 4485  zfrep6 4545  fv3 4690  iotanul 5098  iota4 5100  tfrlem5 5123  dfom3 5737  aceq5 5902  aceq6a 5903  aceq6b 5904  kmlem1 5927  kmlem13 5939  zorn 5959  brdom3 5963  brdom4 5965  axpowndlem2 6102  axacndlem1 6111  axacndlem2 6112  axacndlem3 6113  axacndlem4 6114  axacnd 6116  suppsr2 6375  suppsr3 6376  pre-axsup 6444  peano2nn 7118  islp2 9023  usinuniop 10341  chsscmi 10745  chcmhi 10746  pjnormssi 11740  bnj32OLD 12399  bnj112 12457  bnj876 12803  bnj957 12852  bnj1167 12959  bnj1168 12960  bnj1478 13154  bnj849 13318  bnj1172 13440  bnj1174 13442  trintOLD 13794  elpotr 13847  dfon2lem8 13856  distel 13870  hbimtg 13873  ref4w 14370  inttr 14384  dfiin2gOLD 15356  nninfnub 15819  stdpc4-2 16322  pm11.12 16324  2exim 16331  2exbi 16332  pm11.57 16346  pm11.61 16350  ax4567 16359  ax4567to6 16362  ax4567to7 16363  ax10ext 16364  ax10-16 16365  pm13.192 16374  euunianOLD 16396  rcla4t 16407  ralbidar 16422  rexbidar 16423

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

Copyright terms: Public domain