Theorem 3imp 1111

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3imp31  1112  3imp231  1113  3impb  1115  bi23imp13  1116  3impib  1117  3imp1  1349  3impd  1350  3jao  1428  biimp3ar  1473  3elpr2eq  4850  wefrc  5618  iotan0  6482  f1ssf1  6806  fveqdmss  7024  funelss  7993  poxp  8071  fvn0elsuppb  8124  suppfnss  8132  smo11  8297  odi  8507  omass  8508  nndi  8552  nnmass  8553  undifixp  8875  domunfican  9225  preleqg  9527  dfac8alem  9942  fin33i  10282  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ttukeyg  10430  axdclem  10432  grupr  10711  nqereu  10843  squeeze0  12050  rpnnen1lem5  12922  xnn0lenn0nn0  13188  supxrun  13259  difelfzle  13586  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  elfznelfzo  13719  injresinj  13737  mulexp  14054  expadd  14057  expmul  14060  facdiv  14240  hashgt12el2  14376  hashimarni  14394  leisorel  14413  fi1uzind  14460  pfxfv  14636  swrdswrdlem  14657  pfxccat3  14687  reuccatpfxs1lem  14699  repswswrd  14737  cshf1  14763  2cshwcshw  14778  cshimadifsn  14782  relexpindlem  15016  pwdif  15824  dvdsaddre2b  16267  addmodlteqALT  16285  ltoddhalfle  16321  halfleoddlt  16322  coprmprod  16621  coprmproddvds  16623  cncongr1  16627  oddprmgt2  16660  prmfac1  16681  infpnlem1  16872  prmgaplem5  17017  prmgaplem6  17018  cshwshashlem1  17057  setsstruct  17137  iscatd2  17638  initoeu2lem2  17973  clatleglb  18475  dfgrp3e  19007  mulgaddcom  19065  mulginvcom  19066  symgfvne  19347  lsmcv  21131  assamulgscm  21891  psrvscafval  21937  mat1scmat  22514  cramer0  22665  chpscmat  22817  fvmptnn04ifa  22825  fvmptnn04ifc  22827  fvmptnn04ifd  22828  fiinopn  22876  opnneissb  23089  cnpimaex  23231  regsep  23309  hausnei2  23328  cmpsublem  23374  cmpsub  23375  filufint  23895  blssps  24399  blss  24400  mblsplit  25509  dvply2g  26261  taylply2  26344  bcmono  27254  gausslemma2dlem1a  27342  2sqlem10  27405  eqcuts3  27810  addsuniflem  28007  negsunif  28061  sltmuls2  28154  precsexlem11  28223  bdaypw2n0bndlem  28469  elreno2  28501  elntg2  29068  upgrex  29175  numedglnl  29227  ausgrumgri  29250  ausgrusgri  29251  usgredg2vtxeuALT  29305  ushgredgedg  29312  ushgredgedgloop  29314  edg0usgr  29336  0uhgrsubgr  29362  subumgredg2  29368  fusgrfisbase  29411  cusgrsizeinds  29536  cusgrsize2inds  29537  finsumvtxdg2size  29634  upgrewlkle2  29690  wlkl1loop  29721  pthdivtx  29810  2pthnloop  29814  upgrwlkdvde  29820  uhgrwkspthlem2  29837  usgr2pthlem  29846  usgr2pth  29847  clwlkl1loop  29866  crctcshwlkn0lem4  29896  wwlksnextproplem3  29994  wspn0  30007  umgr2adedgwlkonALT  30030  umgr2wlk  30032  umgr2wlkon  30033  elwwlks2  30052  clwwlkccatlem  30074  umgrclwwlkge2  30076  clwlkclwwlklem2  30085  clwlkclwwlkf1lem2  30090  clwlkclwwlkf  30093  clwwlknlbonbgr1  30124  clwwlkn1loopb  30128  clwwlkel  30131  clwwlkext2edg  30141  clwwlknonex2lem2  30193  clwwlknonex2  30194  clwwlknonex2e  30195  1pthon2v  30238  uhgr3cyclex  30267  eupth2lem3lem6  30318  frgr3vlem1  30358  3cyclfrgrrn1  30370  frgrnbnb  30378  frgrwopreglem4a  30395  2clwwlk2clwwlklem  30431  wlkl0  30452  frgrregord013  30480  frgrregord13  30481  frgrogt3nreg  30482  friendship  30484  chcompl  31328  spansncol  31654  hoaddsub  31902  bnj600  35077  sconnpht  35427  satffunlem  35599  satfvel  35610  msubvrs  35758  funpsstri  35964  imp5p  36509  cntotbnd  38131  clmgmOLD  38186  grpomndo  38210  rngoneglmul  38278  rngonegrmul  38279  zerdivemp1x  38282  qmapeldisjsim  39195  rnqmapeleldisjsim  39197  atlex  39776  cvlexch1  39788  cvlsupr4  39805  cvlsupr5  39806  cvlsupr6  39807  2llnneN  39869  athgt  39916  llnle  39978  lplnle  40000  lvoli2  40041  pmaple  40221  dalawlem10  40340  dalawlem13  40343  dalawlem14  40344  dalaw  40346  lhp2lt  40461  ldilval  40573  cdleme50trn2  41011  cdlemf  41023  cdlemg18b  41139  tendotp  41221  tendospcanN  41483  dihmeetlem3N  41765  dvh4dimlem  41903  pell14qrexpclnn0  43312  pell1qrgap  43320  aomclem2  43501  rngunsnply  43615  dflim5  43775  relexpaddss  44163  rp-simp2  44238  gneispaceel2  44589  bi33imp12  44936  bi13imp23  44937  bi23imp1  44940  bi123imp0  44941  ee333  44952  jaoded  45011  e333  45177  suctrALTcf  45366  suctrALTcfVD  45367  ax6e2ndeqALT  45375  mullimc  46064  mullimcf  46071  f1oresf1o2  47751  fzopredsuc  47784  subsubelfzo0  47787  nnmul2b  47791  2tceilhalfelfzo1  47796  2timesltsqm1  47839  muldvdsfacgt  47846  muldvdsfacm1  47847  elsetpreimafvbi  47863  iccpartimp  47889  iccpartigtl  47895  lswn0  47916  poprelb  47996  fmtnofac1  48045  lighneallem2  48081  lighneallem3  48082  lighneallem4  48085  nprmdvdsfacm1lem2  48096  mogoldbblem  48208  fpprel2  48229  gbegt5  48249  sbgoldbaltlem1  48267  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  clnbgrssedg  48329  grimuhgr  48375  uhgrimedgi  48378  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrim  48422  grimedg  48423  grimgrtri  48437  usgrgrtrirex  48438  isubgr3stgrlem4  48457  grlimgrtri  48491  clnbgr3stgrgrlim  48507  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgcubic  48567  gpg5nbgr3star  48569  lidldomn1  48719  cznnring  48750  rngccatidALTV  48760  ringccatidALTV  48794  scmsuppss  48859  lmodvsmdi  48867  gsumlsscl  48868  lindslinindimp2lem1  48946  lindsrng01  48956  elfzolborelfzop1  49007  fllog2  49056  dignn0flhalflem1  49103  rrxlinesc  49223  itschlc0yqe  49248  itsclc0xyqsol  49256  itscnhlinecirc02p  49273