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  4849  wefrc  5625  iotan0  6488  f1ssf1  6812  fveqdmss  7030  funelss  8000  poxp  8078  fvn0elsuppb  8131  suppfnss  8139  smo11  8304  odi  8514  omass  8515  nndi  8559  nnmass  8560  undifixp  8882  domunfican  9232  preleqg  9536  dfac8alem  9951  fin33i  10291  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ttukeyg  10439  axdclem  10441  grupr  10720  nqereu  10852  squeeze0  12059  rpnnen1lem5  12931  xnn0lenn0nn0  13197  supxrun  13268  difelfzle  13595  elfzo0z  13656  fzofzim  13664  fzo1fzo0n0  13670  elfzodifsumelfzo  13686  elfznelfzo  13728  injresinj  13746  mulexp  14063  expadd  14066  expmul  14069  facdiv  14249  hashgt12el2  14385  hashimarni  14403  leisorel  14422  fi1uzind  14469  pfxfv  14645  swrdswrdlem  14666  pfxccat3  14696  reuccatpfxs1lem  14708  repswswrd  14746  cshf1  14772  2cshwcshw  14787  cshimadifsn  14791  relexpindlem  15025  pwdif  15833  dvdsaddre2b  16276  addmodlteqALT  16294  ltoddhalfle  16330  halfleoddlt  16331  coprmprod  16630  coprmproddvds  16632  cncongr1  16636  oddprmgt2  16669  prmfac1  16690  infpnlem1  16881  prmgaplem5  17026  prmgaplem6  17027  cshwshashlem1  17066  setsstruct  17146  iscatd2  17647  initoeu2lem2  17982  clatleglb  18484  dfgrp3e  19016  mulgaddcom  19074  mulginvcom  19075  symgfvne  19356  lsmcv  21139  assamulgscm  21881  psrvscafval  21927  mat1scmat  22504  cramer0  22655  chpscmat  22807  fvmptnn04ifa  22815  fvmptnn04ifc  22817  fvmptnn04ifd  22818  fiinopn  22866  opnneissb  23079  cnpimaex  23221  regsep  23299  hausnei2  23318  cmpsublem  23364  cmpsub  23365  filufint  23885  blssps  24389  blss  24390  mblsplit  25499  dvply2g  26251  taylply2  26333  bcmono  27240  gausslemma2dlem1a  27328  2sqlem10  27391  eqcuts3  27796  addsuniflem  27993  negsunif  28047  sltmuls2  28140  precsexlem11  28209  bdaypw2n0bndlem  28455  elreno2  28487  elntg2  29054  upgrex  29161  numedglnl  29213  ausgrumgri  29236  ausgrusgri  29237  usgredg2vtxeuALT  29291  ushgredgedg  29298  ushgredgedgloop  29300  edg0usgr  29322  0uhgrsubgr  29348  subumgredg2  29354  fusgrfisbase  29397  cusgrsizeinds  29521  cusgrsize2inds  29522  finsumvtxdg2size  29619  upgrewlkle2  29675  wlkl1loop  29706  pthdivtx  29795  2pthnloop  29799  upgrwlkdvde  29805  uhgrwkspthlem2  29822  usgr2pthlem  29831  usgr2pth  29832  clwlkl1loop  29851  crctcshwlkn0lem4  29881  wwlksnextproplem3  29979  wspn0  29992  umgr2adedgwlkonALT  30015  umgr2wlk  30017  umgr2wlkon  30018  elwwlks2  30037  clwwlkccatlem  30059  umgrclwwlkge2  30061  clwlkclwwlklem2  30070  clwlkclwwlkf1lem2  30075  clwlkclwwlkf  30078  clwwlknlbonbgr1  30109  clwwlkn1loopb  30113  clwwlkel  30116  clwwlkext2edg  30126  clwwlknonex2lem2  30178  clwwlknonex2  30179  clwwlknonex2e  30180  1pthon2v  30223  uhgr3cyclex  30252  eupth2lem3lem6  30303  frgr3vlem1  30343  3cyclfrgrrn1  30355  frgrnbnb  30363  frgrwopreglem4a  30380  2clwwlk2clwwlklem  30416  wlkl0  30437  frgrregord013  30465  frgrregord13  30466  frgrogt3nreg  30467  friendship  30469  chcompl  31313  spansncol  31639  hoaddsub  31887  bnj600  35061  sconnpht  35411  satffunlem  35583  satfvel  35594  msubvrs  35742  funpsstri  35948  imp5p  36493  cntotbnd  38117  clmgmOLD  38172  grpomndo  38196  rngoneglmul  38264  rngonegrmul  38265  zerdivemp1x  38268  qmapeldisjsim  39181  rnqmapeleldisjsim  39183  atlex  39762  cvlexch1  39774  cvlsupr4  39791  cvlsupr5  39792  cvlsupr6  39793  2llnneN  39855  athgt  39902  llnle  39964  lplnle  39986  lvoli2  40027  pmaple  40207  dalawlem10  40326  dalawlem13  40329  dalawlem14  40330  dalaw  40332  lhp2lt  40447  ldilval  40559  cdleme50trn2  40997  cdlemf  41009  cdlemg18b  41125  tendotp  41207  tendospcanN  41469  dihmeetlem3N  41751  dvh4dimlem  41889  pell14qrexpclnn0  43294  pell1qrgap  43302  aomclem2  43483  rngunsnply  43597  dflim5  43757  relexpaddss  44145  rp-simp2  44220  gneispaceel2  44571  bi33imp12  44918  bi13imp23  44919  bi23imp1  44922  bi123imp0  44923  ee333  44934  jaoded  44993  e333  45159  suctrALTcf  45348  suctrALTcfVD  45349  ax6e2ndeqALT  45357  mullimc  46046  mullimcf  46053  f1oresf1o2  47739  fzopredsuc  47772  subsubelfzo0  47775  nnmul2b  47779  2tceilhalfelfzo1  47784  2timesltsqm1  47827  muldvdsfacgt  47834  muldvdsfacm1  47835  elsetpreimafvbi  47851  iccpartimp  47877  iccpartigtl  47883  lswn0  47904  poprelb  47984  fmtnofac1  48033  lighneallem2  48069  lighneallem3  48070  lighneallem4  48073  nprmdvdsfacm1lem2  48084  mogoldbblem  48196  fpprel2  48217  gbegt5  48237  sbgoldbaltlem1  48255  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  clnbgrssedg  48317  grimuhgr  48363  uhgrimedgi  48366  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrim  48410  grimedg  48411  grimgrtri  48425  usgrgrtrirex  48426  isubgr3stgrlem4  48445  grlimgrtri  48479  clnbgr3stgrgrlim  48495  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgcubic  48555  gpg5nbgr3star  48557  lidldomn1  48707  cznnring  48738  rngccatidALTV  48748  ringccatidALTV  48782  scmsuppss  48847  lmodvsmdi  48855  gsumlsscl  48856  lindslinindimp2lem1  48934  lindsrng01  48944  elfzolborelfzop1  48995  fllog2  49044  dignn0flhalflem1  49091  rrxlinesc  49211  itschlc0yqe  49236  itsclc0xyqsol  49244  itscnhlinecirc02p  49261