Theorem 3imp 1110

Description: Importation inference. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jun-2022.)

Hypothesis

Ref	Expression
3imp.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
3imp	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	imp31 417	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1109	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3imp31  1111  3imp231  1112  3impb  1114  bi23imp13  1115  3impib  1116  3imp1  1348  3impd  1349  3jao  1427  biimp3ar  1472  3elpr2eq  4860  wefrc  5617  iotan0  6476  f1ssf1  6800  fveqdmss  7016  funelss  7989  poxp  8068  fvn0elsuppb  8121  suppfnss  8129  smo11  8294  odi  8504  omass  8505  nndi  8548  nnmass  8549  undifixp  8868  domunfican  9230  preleqg  9530  dfac8alem  9942  fin33i  10282  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ttukeyg  10430  axdclem  10432  grupr  10710  nqereu  10842  squeeze0  12046  rpnnen1lem5  12900  xnn0lenn0nn0  13165  supxrun  13236  difelfzle  13562  elfzo0z  13622  fzofzim  13630  fzo1fzo0n0  13636  elfzodifsumelfzo  13652  elfznelfzo  13693  injresinj  13709  mulexp  14026  expadd  14029  expmul  14032  facdiv  14212  hashgt12el2  14348  hashimarni  14366  leisorel  14385  fi1uzind  14432  pfxfv  14607  swrdswrdlem  14628  pfxccat3  14658  reuccatpfxs1lem  14670  repswswrd  14708  cshf1  14734  2cshwcshw  14750  cshimadifsn  14754  relexpindlem  14988  pwdif  15793  dvdsaddre2b  16236  addmodlteqALT  16254  ltoddhalfle  16290  halfleoddlt  16291  coprmprod  16590  coprmproddvds  16592  cncongr1  16596  oddprmgt2  16628  prmfac1  16649  infpnlem1  16840  prmgaplem5  16985  prmgaplem6  16986  cshwshashlem1  17025  setsstruct  17105  iscatd2  17605  initoeu2lem2  17940  clatleglb  18442  dfgrp3e  18937  mulgaddcom  18995  mulginvcom  18996  symgfvne  19278  lsmcv  21066  assamulgscm  21826  psrvscafval  21873  mat1scmat  22442  cramer0  22593  chpscmat  22745  fvmptnn04ifa  22753  fvmptnn04ifc  22755  fvmptnn04ifd  22756  fiinopn  22804  opnneissb  23017  cnpimaex  23159  regsep  23237  hausnei2  23256  cmpsublem  23302  cmpsub  23303  filufint  23823  blssps  24328  blss  24329  mblsplit  25449  dvply2g  26208  taylply2  26291  bcmono  27204  gausslemma2dlem1a  27292  2sqlem10  27355  eqscut3  27753  addsuniflem  27931  negsunif  27984  ssltmul2  28074  precsexlem11  28142  elntg2  28948  upgrex  29055  numedglnl  29107  ausgrumgri  29130  ausgrusgri  29131  usgredg2vtxeuALT  29185  ushgredgedg  29192  ushgredgedgloop  29194  edg0usgr  29216  0uhgrsubgr  29242  subumgredg2  29248  fusgrfisbase  29291  cusgrsizeinds  29416  cusgrsize2inds  29417  finsumvtxdg2size  29514  upgrewlkle2  29570  wlkl1loop  29601  pthdivtx  29690  2pthnloop  29694  upgrwlkdvde  29700  uhgrwkspthlem2  29717  usgr2pthlem  29726  usgr2pth  29727  clwlkl1loop  29746  crctcshwlkn0lem4  29776  wwlksnextproplem3  29874  wspn0  29887  umgr2adedgwlkonALT  29910  umgr2wlk  29912  umgr2wlkon  29913  elwwlks2  29929  clwwlkccatlem  29951  umgrclwwlkge2  29953  clwlkclwwlklem2  29962  clwlkclwwlkf1lem2  29967  clwlkclwwlkf  29970  clwwlknlbonbgr1  30001  clwwlkn1loopb  30005  clwwlkel  30008  clwwlkext2edg  30018  clwwlknonex2lem2  30070  clwwlknonex2  30071  clwwlknonex2e  30072  1pthon2v  30115  uhgr3cyclex  30144  eupth2lem3lem6  30195  frgr3vlem1  30235  3cyclfrgrrn1  30247  frgrnbnb  30255  frgrwopreglem4a  30272  2clwwlk2clwwlklem  30308  wlkl0  30329  frgrregord013  30357  frgrregord13  30358  frgrogt3nreg  30359  friendship  30361  chcompl  31204  spansncol  31530  hoaddsub  31778  bnj600  34885  sconnpht  35201  satffunlem  35373  satfvel  35384  msubvrs  35532  funpsstri  35738  imp5p  36284  cntotbnd  37775  clmgmOLD  37830  grpomndo  37854  rngoneglmul  37922  rngonegrmul  37923  zerdivemp1x  37926  atlex  39294  cvlexch1  39306  cvlsupr4  39323  cvlsupr5  39324  cvlsupr6  39325  2llnneN  39388  athgt  39435  llnle  39497  lplnle  39519  lvoli2  39560  pmaple  39740  dalawlem10  39859  dalawlem13  39862  dalawlem14  39863  dalaw  39865  lhp2lt  39980  ldilval  40092  cdleme50trn2  40530  cdlemf  40542  cdlemg18b  40658  tendotp  40740  tendospcanN  41002  dihmeetlem3N  41284  dvh4dimlem  41422  pell14qrexpclnn0  42839  pell1qrgap  42847  aomclem2  43028  rngunsnply  43142  dflim5  43302  relexpaddss  43691  rp-simp2  43766  gneispaceel2  44117  bi33imp12  44465  bi13imp23  44466  bi23imp1  44469  bi123imp0  44470  ee333  44481  jaoded  44540  e333  44706  suctrALTcf  44895  suctrALTcfVD  44896  ax6e2ndeqALT  44904  mullimc  45598  mullimcf  45605  f1oresf1o2  47276  fzopredsuc  47308  subsubelfzo0  47311  2tceilhalfelfzo1  47317  elsetpreimafvbi  47376  iccpartimp  47402  iccpartigtl  47408  lswn0  47429  poprelb  47509  fmtnofac1  47555  lighneallem2  47591  lighneallem3  47592  lighneallem4  47595  mogoldbblem  47705  fpprel2  47726  gbegt5  47746  sbgoldbaltlem1  47764  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  clnbgrssedg  47826  grimuhgr  47872  uhgrimedgi  47875  uhgrimisgrgriclem  47915  uhgrimisgrgric  47916  clnbgrgrim  47919  grimedg  47920  grimgrtri  47934  usgrgrtrirex  47935  isubgr3stgrlem4  47954  grlimgrtri  47988  clnbgr3stgrgrlim  48004  gpgedgvtx1  48047  gpgvtxedg0  48048  gpgvtxedg1  48049  gpgcubic  48064  gpg5nbgr3star  48066  lidldomn1  48216  cznnring  48247  rngccatidALTV  48257  ringccatidALTV  48291  scmsuppss  48356  lmodvsmdi  48364  gsumlsscl  48365  lindslinindimp2lem1  48444  lindsrng01  48454  elfzolborelfzop1  48505  fllog2  48554  dignn0flhalflem1  48601  rrxlinesc  48721  itschlc0yqe  48746  itsclc0xyqsol  48754  itscnhlinecirc02p  48771