Theorem con4d 105

Description: Deduction derived from axiom ax-3 8. (Contributed by NM, 26-Mar-1995.)

Hypothesis

Ref	Expression
con4d.1

Assertion

Ref	Expression
con4d

Proof of Theorem con4d

Step	Hyp	Ref	Expression
1		con4d.1	. 2
2		ax-3 8	. 2
3	1, 2	syl 16	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  pm2.21d  106  pm2.18  110  con2d  115  con1d  124  mt4d  138  impcon4bid  205  con4bid  293  aleximi  1653  eximOLD  1655  necon2adOLD  2671  spc2gv  3197  spc3gv  3199  soisoi  6224  isomin  6233  riotaclb  6295  extmptsuppeq  6943  mpt2xopynvov0g  6961  boxcutc  7532  sdomel  7684  onsdominel  7686  preleq  8055  cflim2  8664  cfslbn  8668  cofsmo  8670  fincssdom  8724  fin23lem25  8725  fin23lem26  8726  fin1a2s  8815  pwfseqlem4  9061  ltapr  9444  suplem2pr  9452  qsqueeze  11429  ssfzoulel  11906  ssnn0fi  12094  hashbnd  12411  hashclb  12430  hashgt0elex  12466  hashgt12el  12481  hashgt12el2  12482  pc2dvds  14402  infpnlem1  14428  odcl2  16587  ufilmax  20408  ufileu  20420  filufint  20421  hausflim  20482  flimfnfcls  20529  alexsubALTlem3  20549  alexsubALTlem4  20550  reconnlem2  21332  lebnumlem3  21463  rrxmvallem  21831  itg1ge0a  22118  itg2seq  22149  m1lgs  23637  lmieu  24150  axlowdimlem14  24258  usgraidx2v  24393  cusgrafilem3  24481  cusgrafi  24482  usgrcyclnl1  24640  ex-natded5.13-2  25137  ordtconlem1  27906  eulerpartlemgh  28317  wfi  29287  frind  29323  meran1  29876  nn0prpw  30141  heiborlem1  30307  limclr  31661  eu2ndop1stv  32207  usgedgvadf1  32415  usgedgvadf1ALT  32418  mndpsuppss  32964  bnj23  33771  riotaclbgBAD  34685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8