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  4858  wefrc  5610  iotan0  6471  f1ssf1  6795  fveqdmss  7011  funelss  7979  poxp  8058  fvn0elsuppb  8111  suppfnss  8119  smo11  8284  odi  8494  omass  8495  nndi  8538  nnmass  8539  undifixp  8858  domunfican  9206  preleqg  9505  dfac8alem  9917  fin33i  10257  domtriomlem  10330  axdc3lem2  10339  axdc3lem4  10341  axdc4lem  10343  ttukeyg  10405  axdclem  10407  grupr  10685  nqereu  10817  squeeze0  12022  rpnnen1lem5  12876  xnn0lenn0nn0  13141  supxrun  13212  difelfzle  13538  elfzo0z  13598  fzofzim  13606  fzo1fzo0n0  13612  elfzodifsumelfzo  13628  elfznelfzo  13670  injresinj  13688  mulexp  14005  expadd  14008  expmul  14011  facdiv  14191  hashgt12el2  14327  hashimarni  14345  leisorel  14364  fi1uzind  14411  pfxfv  14587  swrdswrdlem  14608  pfxccat3  14638  reuccatpfxs1lem  14650  repswswrd  14688  cshf1  14714  2cshwcshw  14729  cshimadifsn  14733  relexpindlem  14967  pwdif  15772  dvdsaddre2b  16215  addmodlteqALT  16233  ltoddhalfle  16269  halfleoddlt  16270  coprmprod  16569  coprmproddvds  16571  cncongr1  16575  oddprmgt2  16607  prmfac1  16628  infpnlem1  16819  prmgaplem5  16964  prmgaplem6  16965  cshwshashlem1  17004  setsstruct  17084  iscatd2  17584  initoeu2lem2  17919  clatleglb  18421  dfgrp3e  18950  mulgaddcom  19008  mulginvcom  19009  symgfvne  19291  lsmcv  21076  assamulgscm  21836  psrvscafval  21883  mat1scmat  22452  cramer0  22603  chpscmat  22755  fvmptnn04ifa  22763  fvmptnn04ifc  22765  fvmptnn04ifd  22766  fiinopn  22814  opnneissb  23027  cnpimaex  23169  regsep  23247  hausnei2  23266  cmpsublem  23312  cmpsub  23313  filufint  23833  blssps  24337  blss  24338  mblsplit  25458  dvply2g  26217  taylply2  26300  bcmono  27213  gausslemma2dlem1a  27301  2sqlem10  27364  eqscut3  27763  addsuniflem  27942  negsunif  27995  ssltmul2  28085  precsexlem11  28153  elntg2  28961  upgrex  29068  numedglnl  29120  ausgrumgri  29143  ausgrusgri  29144  usgredg2vtxeuALT  29198  ushgredgedg  29205  ushgredgedgloop  29207  edg0usgr  29229  0uhgrsubgr  29255  subumgredg2  29261  fusgrfisbase  29304  cusgrsizeinds  29429  cusgrsize2inds  29430  finsumvtxdg2size  29527  upgrewlkle2  29583  wlkl1loop  29614  pthdivtx  29703  2pthnloop  29707  upgrwlkdvde  29713  uhgrwkspthlem2  29730  usgr2pthlem  29739  usgr2pth  29740  clwlkl1loop  29759  crctcshwlkn0lem4  29789  wwlksnextproplem3  29887  wspn0  29900  umgr2adedgwlkonALT  29923  umgr2wlk  29925  umgr2wlkon  29926  elwwlks2  29942  clwwlkccatlem  29964  umgrclwwlkge2  29966  clwlkclwwlklem2  29975  clwlkclwwlkf1lem2  29980  clwlkclwwlkf  29983  clwwlknlbonbgr1  30014  clwwlkn1loopb  30018  clwwlkel  30021  clwwlkext2edg  30031  clwwlknonex2lem2  30083  clwwlknonex2  30084  clwwlknonex2e  30085  1pthon2v  30128  uhgr3cyclex  30157  eupth2lem3lem6  30208  frgr3vlem1  30248  3cyclfrgrrn1  30260  frgrnbnb  30268  frgrwopreglem4a  30285  2clwwlk2clwwlklem  30321  wlkl0  30342  frgrregord013  30370  frgrregord13  30371  frgrogt3nreg  30372  friendship  30374  chcompl  31217  spansncol  31543  hoaddsub  31791  bnj600  34926  sconnpht  35261  satffunlem  35433  satfvel  35444  msubvrs  35592  funpsstri  35798  imp5p  36344  cntotbnd  37835  clmgmOLD  37890  grpomndo  37914  rngoneglmul  37982  rngonegrmul  37983  zerdivemp1x  37986  atlex  39354  cvlexch1  39366  cvlsupr4  39383  cvlsupr5  39384  cvlsupr6  39385  2llnneN  39447  athgt  39494  llnle  39556  lplnle  39578  lvoli2  39619  pmaple  39799  dalawlem10  39918  dalawlem13  39921  dalawlem14  39922  dalaw  39924  lhp2lt  40039  ldilval  40151  cdleme50trn2  40589  cdlemf  40601  cdlemg18b  40717  tendotp  40799  tendospcanN  41061  dihmeetlem3N  41343  dvh4dimlem  41481  pell14qrexpclnn0  42898  pell1qrgap  42906  aomclem2  43087  rngunsnply  43201  dflim5  43361  relexpaddss  43750  rp-simp2  43825  gneispaceel2  44176  bi33imp12  44523  bi13imp23  44524  bi23imp1  44527  bi123imp0  44528  ee333  44539  jaoded  44598  e333  44764  suctrALTcf  44953  suctrALTcfVD  44954  ax6e2ndeqALT  44962  mullimc  45655  mullimcf  45662  f1oresf1o2  47321  fzopredsuc  47353  subsubelfzo0  47356  2tceilhalfelfzo1  47362  elsetpreimafvbi  47421  iccpartimp  47447  iccpartigtl  47453  lswn0  47474  poprelb  47554  fmtnofac1  47600  lighneallem2  47636  lighneallem3  47637  lighneallem4  47640  mogoldbblem  47750  fpprel2  47771  gbegt5  47791  sbgoldbaltlem1  47809  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  clnbgrssedg  47871  grimuhgr  47917  uhgrimedgi  47920  uhgrimisgrgriclem  47960  uhgrimisgrgric  47961  clnbgrgrim  47964  grimedg  47965  grimgrtri  47979  usgrgrtrirex  47980  isubgr3stgrlem4  47999  grlimgrtri  48033  clnbgr3stgrgrlim  48049  gpgedgvtx1  48092  gpgvtxedg0  48093  gpgvtxedg1  48094  gpgcubic  48109  gpg5nbgr3star  48111  lidldomn1  48261  cznnring  48292  rngccatidALTV  48302  ringccatidALTV  48336  scmsuppss  48401  lmodvsmdi  48409  gsumlsscl  48410  lindslinindimp2lem1  48489  lindsrng01  48499  elfzolborelfzop1  48550  fllog2  48599  dignn0flhalflem1  48646  rrxlinesc  48766  itschlc0yqe  48791  itsclc0xyqsol  48799  itscnhlinecirc02p  48816