MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imp Structured version   Visualization version   GIF version

Theorem 3imp 1248
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
3imp ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 1032 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 446 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 205 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3imp31  1249  3impa  1250  3impb  1251  3impia  1252  3impib  1253  3com23  1262  3imp21  1268  3imp3i2an  1269  3an1rs  1270  3imp1  1271  3impd  1272  syl3an2  1351  syl3an3  1352  3jao  1380  biimp3ar  1424  wefrc  5019  sotri2  5428  predpo  5598  fveqdmss  6244  poxp  7150  fvn0elsuppb  7173  smo11  7322  oawordri  7491  odi  7520  omass  7521  nndi  7564  nnmass  7565  undifixp  7804  isinf  8032  domunfican  8092  infssuni  8114  pr2nelem  8684  dfac8alem  8709  fin33i  9048  fin1a2lem10  9088  domtriomlem  9121  axdc3lem2  9130  axdc3lem4  9132  axdc4lem  9134  ttukeyg  9196  axdclem  9198  grupr  9472  nqereu  9604  squeeze0  10772  rpnnen1lem5  11647  rpnnen1lem5OLD  11653  supxrun  11971  difelfzle  12273  elfzo0z  12329  fzofzim  12334  fzo1fzo0n0  12338  elfzodifsumelfzo  12353  elfznelfzo  12391  injresinj  12403  mulexp  12713  expadd  12716  expmul  12719  bernneq  12804  facdiv  12888  hashgt12el2  13020  hashimarni  13035  leisorel  13050  fi1uzind  13077  fi1uzindOLD  13083  2swrd1eqwrdeq  13249  swrdswrdlem  13254  swrdccat3  13286  swrdccatid  13291  repswswrd  13325  cshf1  13350  2cshwcshw  13365  cshimadifsn  13369  swrdco  13377  relexpindlem  13594  dvdsaddre2b  14810  addmodlteqALT  14828  ltoddhalfle  14866  halfleoddlt  14867  dfgcd2  15044  coprmprod  15156  coprmproddvds  15158  cncongr1  15162  oddprmgt2  15192  prmfac1  15212  infpnlem1  15395  prmgaplem5  15540  prmgaplem6  15541  cshwshashlem1  15583  iscatd2  16108  initoeu2lem2  16431  clatleglb  16892  dfgrp3e  17281  mulgaddcom  17330  mulginvcom  17331  symgfvne  17574  f1rhm0to0ALT  18507  lmodvsmmulgdi  18664  lsmcv  18905  assamulgscm  19114  psrvscafval  19154  mamufacex  19953  mat1scmat  20103  gsummatr01lem4  20222  cramer0  20254  chpscmat  20405  fvmptnn04ifa  20413  fvmptnn04ifc  20415  fvmptnn04ifd  20416  fiinopn  20470  opnneissb  20667  cnpimaex  20809  regsep  20887  hausnei2  20906  cmpsublem  20951  cmpsub  20952  filufint  21473  blssps  21977  blss  21978  mblsplit  23021  bcmono  24716  gausslemma2dlem1a  24804  2sqlem10  24867  usgraedg4  25679  usgrafisinds  25705  nbgraf1olem3  25735  cusgrasizeinds  25767  cusgrasize2inds  25768  1pthoncl  25885  2pthoncl  25896  wlkdvspthlem  25900  wlkdvspth  25901  usgra2adedgwlkonALT  25907  usgra2wlkspthlem1  25910  usgra2wlkspth  25912  3v3e3cycl1  25935  constr3trl  25950  constr3pth  25951  constr3cycl  25952  4cycl4v4e  25957  4cycl4dv  25958  4cycl4dv4e  25959  wwlkm1edg  26026  wwlkextproplem3  26034  clwlkisclwwlklem1  26078  clwwlkel  26084  clwwlkext2edg  26093  usg2cwwk2dif  26111  clwlkf1clwwlklem  26139  el2wlkonot  26159  el2spthonot  26160  el2spthonot0  26161  el2wlkonotot0  26162  usg2wlkonot  26173  usg2wotspth  26174  cusgraiffrusgra  26230  rusgrasn  26235  eupatrl  26258  frgraunss  26285  3cyclfrgrarn1  26302  frgranbnb  26310  vdfrgra0  26312  usgn0fidegnn0  26319  frgrawopreglem2  26335  frgrawopreglem5  26338  clwwlkextfrlem1  26366  numclwwlkovf2ex  26376  extwwlkfab  26380  numclwlk1lem2foa  26381  frgraregord013  26408  frgraregord13  26409  frgraogt3nreg  26410  friendship  26412  chcompl  27286  spansncol  27614  hoaddsub  27862  bnj600  30046  sconpht  30268  msubvrs  30514  funpsstri  30712  imp5p  31278  cntotbnd  32565  clmgmOLD  32620  grpomndo  32644  rngoneglmul  32712  rngonegrmul  32713  zerdivemp1x  32716  atlex  33421  cvlexch1  33433  cvlsupr4  33450  cvlsupr5  33451  cvlsupr6  33452  2llnneN  33513  athgt  33560  llnle  33622  lplnle  33644  lvoli2  33685  pmaple  33865  dalawlem10  33984  dalawlem13  33987  dalawlem14  33988  dalaw  33990  lhp2lt  34105  ldilval  34217  cdleme50trn2  34657  cdlemf  34669  cdlemg18b  34785  tendotp  34867  tendospcanN  35130  dihmeetlem3N  35412  dvh4dimlem  35550  pell14qrexpclnn0  36248  pell1qrgap  36256  aomclem2  36443  rngunsnply  36562  relexpxpmin  36828  relexpaddss  36829  rp-simp2  36907  gneispaceel2  37262  bi33imp12  37517  bi23imp13  37518  bi13imp23  37519  bi23imp1  37522  bi123imp0  37523  ee333  37534  jaoded  37603  eel12131  37759  e333  37781  3imp231  37866  suctrALTcf  37980  suctrALTcfVD  37981  ax6e2ndeqALT  37989  mullimc  38484  mullimcf  38491  fzopredsuc  39748  iccpartimp  39757  iccpartigtl  39763  fmtnofac1  39822  pwdif  39841  lighneallem2  39863  lighneallem3  39864  lighneallem4  39867  gbegt5  39985  sgoldbaltlem1  40003  bgoldbtbndlem2  40024  bgoldbtbndlem3  40025  lswn0  40044  pfxfv  40064  pfxccat3  40091  reuccatpfxs1lem  40098  f1ssf1  40144  subsubelfzo0  40183  uhgrauhgrbi  40293  upgrex  40317  ausgrumgri  40396  ausgrusgri  40397  usgredg2vtxeuALT  40448  ushgredgedga  40455  ushgredgedgaloop  40457  edg0usgr  40478  0uhgrsubgr  40502  subumgredg2  40508  fusgrfisbase  40546  cusgrsizeinds  40667  cusgrsize2inds  40668  upgrewlkle2  40807  1wlkl1loop  40841  pthdivtx  40934  2pthnloop  40936  upgrwlkdvde  40942  uhgr1wlkspthlem2  40959  usgr2pthlem  40968  usgr2pth  40969  clwlkl1loop  40988  cyclnsPth  41005  crctcsh1wlkn0lem4  41015  wwlksnextproplem3  41116  umgr2adedgwlkonALT  41153  umgr2wlk  41155  umgr2wlkon  41156  elwwlks2  41169  clwlkclwwlklem2  41208  umgrclwwlksge2  41218  clwwlksel  41220  clwwlksext2edg  41229  clwwnisshclwwsn  41236  1pthon2v-av  41319  uhgr3cyclex  41348  eupth2lem3lem6  41400  frgr3vlem1  41442  3cyclfrgrrn1  41454  frgrnbnb  41462  frgrwopreglem5  41484  av-numclwwlkovf2ex  41516  av-extwwlkfab  41519  av-numclwlk1lem2foa  41520  av-frgraregord013  41548  av-frgraregord13  41549  av-frgraogt3nreg  41550  av-friendship  41552  lidldomn1  41710  cznnring  41747  rngccatidALTV  41780  ringccatidALTV  41843  scmsuppss  41946  lmodvsmdi  41956  gsumlsscl  41957  lindslinindimp2lem1  42040  lindsrng01  42050  elfzolborelfzop1  42102  difmodm1lt  42110  fllog2  42159  dignn0flhalflem1  42206
  Copyright terms: Public domain W3C validator