Theorem impd 431

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
imp3.1

Assertion

Ref	Expression
impd

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		imp3.1	. . . 4
2	1	com3l 81	. . 3
3	2	imp 429	. 2
4	3	com12 31	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  imp32  433  pm3.31  445  syland  481  imp4c  591  imp4d  592  imp5d  599  expimpd  603  expl  618  3expib  1199  axc9lem1  2001  equs5  2092  rsp2  2831  moi  3282  reu6  3288  sbciegft  3358  elpwunsn  4070  prel12  4207  opthpr  4208  invdisj  4441  reusv1  4652  sotr2  4834  wefrc  4878  tz7.7  4909  ordtr2  4927  relop  5158  elres  5314  iss  5326  funssres  5633  fv3  5884  fmptsnd  6093  funfvima  6147  isomin  6233  sorpsscmpl  6591  peano5  6723  f1oweALT  6784  poxp  6912  soxp  6913  tfr3  7087  tz7.48-1  7127  omordi  7234  odi  7247  omass  7248  oen0  7254  nndi  7291  nnmass  7292  nnmordi  7299  nnmord  7300  eroveu  7425  findcard3  7783  fiint  7817  suplub  7940  hartogs  7990  card2on  8001  unxpwdom2  8035  inf3lem2  8067  epfrs  8183  tcel  8197  dfac2  8532  cfcoflem  8673  infpssr  8709  isf32lem9  8762  axdc3lem4  8854  axcclem  8858  zorn2lem7  8903  ttukeylem6  8915  brdom6disj  8931  ondomon  8959  inar1  9174  gruen  9211  indpi  9306  nqereu  9328  genpn0  9402  distrlem1pr  9424  distrlem5pr  9426  ltexprlem1  9435  reclem4pr  9449  addsrmo  9471  mulsrmo  9472  supsrlem  9509  lelttr  9696  ltletr  9697  ltlen  9707  mulgt1  10426  fzind  10987  eqreznegel  11196  xrlelttr  11388  xrltletr  11389  fzen  11732  elfzodifsumelfzo  11882  bernneq  12292  swrdswrdlem  12684  wrd2ind  12703  reuccats1lem  12705  swrdccatin1  12708  repsdf2  12750  limsupbnd2  13306  rlimuni  13373  mulcn2  13418  rlimno1  13476  prodmolem2  13742  ndvdssub  14065  coprmdvds  14243  coprmdvds2  14244  maxprmfct  14254  pceu  14370  infpnlem1  14428  imasaddfnlem  14925  plelttr  15602  gsumval2a  15906  symgfix2  16441  gsmsymgrfixlem1  16452  psgnunilem4  16522  lsmmod  16693  lsmdisj2  16700  efgrelexlemb  16768  pgpfac1lem5  17130  lindfrn  18856  mat1dimcrng  18979  dmatelnd  18998  mdetunilem7  19120  cpmatacl  19217  cpmatmcllem  19219  chfacfisf  19355  chfacfisfcpmat  19356  lmss  19799  lmcnp  19805  hausnei2  19854  isnrm2  19859  isnrm3  19860  cmpsublem  19899  2ndcdisj  19957  1stccnp  19963  txcnpi  20109  txlm  20149  tx1stc  20151  fgss2  20375  fgfil  20376  fgcl  20379  ufileu  20420  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  ufilcmp  20533  cnpfcf  20542  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  tmdgsum2  20595  tsmsxp  20657  prdsxmslem2  21032  ivthlem2  21864  ivthlem3  21865  ovolicc2  21933  volfiniun  21957  dyadmax  22007  ellimc3  22283  dvlip2  22396  dvne0  22412  axcontlem4  24270  usgra2edg  24382  usgrares1  24410  nb3graprlem1  24451  iswlkg  24524  usgrcyclnl1  24640  nvnencycllem  24643  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wwlknred  24723  erclwwlktr  24815  erclwwlkntr  24827  clwlkfoclwwlk  24845  el2wlkonotot0  24872  frg2woteq  25060  numclwwlkovf2ex  25086  frgraregord013  25118  gxnn0add  25276  gxadd  25277  gxnn0mul  25279  gxmul  25280  isch3  26159  ocin  26214  shmodsi  26307  spansneleq  26488  stj  27154  atom1d  27272  atcvat2i  27306  chirredlem1  27309  chirredi  27313  mdsymlem3  27324  mdsymlem6  27327  pconcon  28676  cvmsss2  28719  cvmliftlem7  28736  mclsind  28930  dfpo2  29184  dfon2lem9  29223  dfon2  29224  wfr3g  29342  frr3g  29386  frrlem11  29399  cgrextend  29658  btwntriv2  29662  btwncomim  29663  btwnexch3  29670  funtransport  29681  ifscgr  29694  colinearxfr  29725  lineext  29726  fscgr  29730  outsideoftr  29779  itg2addnclem3  30068  itg2addnc  30069  areacirc  30112  trer  30134  finminlem  30136  fnessref  30175  fgmin  30188  ismtybndlem  30302  heibor1lem  30305  prtlem17  30617  pellexlem5  30769  pellex  30771  pell1234qrmulcl  30791  pellfundex  30822  ralxfrd2  32303  usgpredgv  32399  usgpredgvALT  32400  tpres  32554  initoeu1  32617  termoeu1  32624  nzerooringczr  32880  ldepspr  33074  aacllem  33216  19.41rg  33323  iunconlem2  33735  bnj849  33983  bj-andnotim  34177  bj-alanim  34204  bj-equs5v  34332  riotasvd  34687  lshpsmreu  34834  atnle  35042  cvratlem  35145  cvrat2  35153  3dim1  35191  2llnjN  35291  2lplnj  35344  linepsubN  35476  pmapsub  35492  paddasslem14  35557  pclfinN  35624  ispsubcl2N  35671  pclfinclN  35674  ldilval  35837  trlord  36295  cdlemk36  36639  dihlsscpre  36961  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439

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

This theorem depends on definitions:  df-bi 185  df-an 371