MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp3a Unicode version

Theorem imp3a 424
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1
Assertion
Ref Expression
imp3a

Proof of Theorem imp3a
StepHypRef Expression
1 imp3.1 . . . 4
21com3l 78 . . 3
32imp 422 . 2
43com12 30 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362
This theorem is referenced by:  imp32  426  pm3.31  436  syland  471  imp4c  578  imp4d  579  imp5d  586  expimpd  590  expl  605  3expib  1175  axc9lem1  1936  equs5  2033  sbiedOLD  2092  rsp2  2757  moi  3120  reu6  3126  sbciegft  3194  elpwunsn  3894  prel12  4024  opthpr  4025  invdisj  4256  reusv1  4464  sotr2  4641  wefrc  4685  tz7.7  4716  ordtr2  4734  relop  4961  elres  5117  iss  5126  funssres  5430  fv3  5673  funfvima  5920  isomin  5996  sorpsscmpl  6341  peano5  6469  f1oweALT  6530  poxp  6653  soxp  6654  tfr3  6817  tz7.48-1  6857  omordi  6966  odi  6979  omass  6980  oen0  6986  nndi  7023  nnmass  7024  nnmordi  7031  nnmord  7032  eroveu  7156  findcard3  7514  fiint  7547  suplub  7657  hartogs  7705  card2on  7716  unxpwdom2  7750  inf3lem2  7782  epfrs  7898  tcel  7912  dfac2  8247  cfcoflem  8388  infpssr  8424  isf32lem9  8477  axdc3lem4  8569  axcclem  8573  zorn2lem7  8618  ttukeylem6  8630  brdom6disj  8646  ondomon  8674  inar1  8888  gruen  8925  indpi  9022  nqereu  9044  genpn0  9118  distrlem1pr  9140  distrlem5pr  9142  ltexprlem1  9151  reclem4pr  9165  mulcmpblnr  9187  supsrlem  9224  lelttr  9411  ltletr  9412  ltlen  9422  mulgt1  10134  fzind  10685  eqreznegel  10885  xrlelttr  11075  xrltletr  11076  fzen  11411  elfzodifsumelfzo  11545  bernneq  11931  swrdswrdlem  12294  wrd2ind  12313  swrdccatin1  12315  repsdf2  12357  limsupbnd2  12902  rlimuni  12969  mulcn2  13014  rlimno1  13072  ndvdssub  13551  coprmdvds  13728  coprmdvds2  13729  maxprmfct  13739  pceu  13853  infpnlem1  13911  imasaddfnlem  14406  plelttr  15082  gsumval2a  15449  symgfix2  15858  gsmsymgrfixlem1  15869  psgnunilem4  15940  lsmmod  16109  lsmdisj2  16116  efgrelexlemb  16184  pgpfac1lem5  16446  lindfrn  17949  mdetunilem7  18126  lmss  18606  lmcnp  18612  hausnei2  18661  isnrm2  18666  isnrm3  18667  cmpsublem  18706  2ndcdisj  18764  1stccnp  18770  txcnpi  18885  txlm  18925  tx1stc  18927  fgss2  19151  fgfil  19152  fgcl  19155  ufileu  19196  rnelfm  19230  fmfnfmlem2  19232  fmfnfmlem4  19234  fmfnfm  19235  ufilcmp  19309  cnpfcf  19318  alexsubALTlem2  19324  alexsubALTlem4  19326  alexsubALT  19327  tmdgsum2  19371  tsmsxp  19429  prdsxmslem2  19804  ivthlem2  20636  ivthlem3  20637  ovolicc2  20705  volfiniun  20728  dyadmax  20778  ellimc3  21054  dvlip2  21167  dvne0  21183  axcontlem4  22892  usgra2edg  22980  usgrares1  23002  nb3graprlem1  23038  usgrcyclnl1  23205  nvnencycllem  23208  3v3e3cycl1  23209  4cycl4v4e  23231  4cycl4dv4e  23233  gxnn0add  23440  gxadd  23441  gxnn0mul  23443  gxmul  23444  isch3  24323  ocin  24378  shmodsi  24471  spansneleq  24652  stj  25318  atom1d  25436  atcvat2i  25470  chirredlem1  25473  chirredi  25477  mdsymlem3  25488  mdsymlem6  25491  pconcon  26823  cvmsss2  26866  cvmliftlem7  26883  prodmolem2  27150  dfpo2  27267  dfon2lem9  27306  dfon2  27307  wfr3g  27425  frr3g  27469  frrlem11  27482  cgrextend  27741  btwntriv2  27745  btwncomim  27746  btwnexch3  27753  funtransport  27764  ifscgr  27777  colinearxfr  27808  lineext  27809  fscgr  27813  outsideoftr  27862  itg2addnclem3  28116  itg2addnc  28117  areacirc  28160  trer  28182  finminlem  28184  fnessref  28236  fgmin  28262  ismtybndlem  28376  heibor1lem  28379  prtlem17  28693  pellexlem5  28847  pellex  28849  pell1234qrmulcl  28869  pellfundex  28900  ralxfrd2  29811  iswlkg  29959  wwlknred  30029  el2wlkonotot0  30065  erclwwlktr  30159  erclwwlkntr  30175  clwlkfoclwwlk  30192  frg2woteq  30327  numclwwlkovf2ex  30353  frgraregord013  30385  ldepspr  30591  19.41rg  30836  iunconlem2  31249  bnj849  31496  bj-andnotim  31648  bj-alanim  31682  bj-equs5v  31772  riotasvd  32044  lshpsmreu  32191  atnle  32399  cvratlem  32502  cvrat2  32510  3dim1  32548  2llnjN  32648  2lplnj  32701  linepsubN  32833  pmapsub  32849  paddasslem14  32914  pclfinN  32981  ispsubcl2N  33028  pclfinclN  33031  ldilval  33194  trlord  33650  cdlemk36  33994  dihlsscpre  34316  baerlem3lem2  34792  baerlem5alem2  34793  baerlem5blem2  34794
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 179  df-an 364
  Copyright terms: Public domain W3C validator