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  3impib  1115  3imp1  1346  3impd  1347  3jao  1424  biimp3ar  1469  3elpr2eq  4910  wefrc  5682  iotan0  6552  f1ssf1  6880  fveqdmss  7097  funelss  8070  poxp  8151  fvn0elsuppb  8204  suppfnss  8212  smo11  8402  odi  8615  omass  8616  nndi  8659  nnmass  8660  undifixp  8972  domunfican  9358  preleqg  9652  pr2nelemOLD  10040  dfac8alem  10066  fin33i  10406  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  ttukeyg  10554  axdclem  10556  grupr  10834  nqereu  10966  squeeze0  12168  rpnnen1lem5  13020  xnn0lenn0nn0  13283  supxrun  13354  difelfzle  13677  elfzo0z  13737  fzofzim  13745  fzo1fzo0n0  13750  elfzodifsumelfzo  13766  elfznelfzo  13807  injresinj  13823  mulexp  14138  expadd  14141  expmul  14144  facdiv  14322  hashgt12el2  14458  hashimarni  14476  leisorel  14495  fi1uzind  14542  pfxfv  14716  swrdswrdlem  14738  pfxccat3  14768  reuccatpfxs1lem  14780  repswswrd  14818  cshf1  14844  2cshwcshw  14860  cshimadifsn  14864  relexpindlem  15098  pwdif  15900  dvdsaddre2b  16340  addmodlteqALT  16358  ltoddhalfle  16394  halfleoddlt  16395  coprmprod  16694  coprmproddvds  16696  cncongr1  16700  oddprmgt2  16732  prmfac1  16753  infpnlem1  16943  prmgaplem5  17088  prmgaplem6  17089  cshwshashlem1  17129  setsstruct  17209  iscatd2  17725  initoeu2lem2  18068  clatleglb  18575  dfgrp3e  19070  mulgaddcom  19128  mulginvcom  19129  symgfvne  19412  lsmcv  21160  assamulgscm  21938  psrvscafval  21985  mat1scmat  22560  cramer0  22711  chpscmat  22863  fvmptnn04ifa  22871  fvmptnn04ifc  22873  fvmptnn04ifd  22874  fiinopn  22922  opnneissb  23137  cnpimaex  23279  regsep  23357  hausnei2  23376  cmpsublem  23422  cmpsub  23423  filufint  23943  blssps  24449  blss  24450  mblsplit  25580  dvply2g  26340  taylply2  26423  bcmono  27335  gausslemma2dlem1a  27423  2sqlem10  27486  addsuniflem  28048  negsunif  28101  ssltmul2  28188  precsexlem11  28255  elntg2  29014  upgrex  29123  numedglnl  29175  ausgrumgri  29198  ausgrusgri  29199  usgredg2vtxeuALT  29253  ushgredgedg  29260  ushgredgedgloop  29262  edg0usgr  29284  0uhgrsubgr  29310  subumgredg2  29316  fusgrfisbase  29359  cusgrsizeinds  29484  cusgrsize2inds  29485  finsumvtxdg2size  29582  upgrewlkle2  29638  wlkl1loop  29670  pthdivtx  29761  2pthnloop  29763  upgrwlkdvde  29769  uhgrwkspthlem2  29786  usgr2pthlem  29795  usgr2pth  29796  clwlkl1loop  29815  crctcshwlkn0lem4  29842  wwlksnextproplem3  29940  wspn0  29953  umgr2adedgwlkonALT  29976  umgr2wlk  29978  umgr2wlkon  29979  elwwlks2  29995  clwwlkccatlem  30017  umgrclwwlkge2  30019  clwlkclwwlklem2  30028  clwlkclwwlkf1lem2  30033  clwlkclwwlkf  30036  clwwlknlbonbgr1  30067  clwwlkn1loopb  30071  clwwlkel  30074  clwwlkext2edg  30084  clwwlknonex2lem2  30136  clwwlknonex2  30137  clwwlknonex2e  30138  1pthon2v  30181  uhgr3cyclex  30210  eupth2lem3lem6  30261  frgr3vlem1  30301  3cyclfrgrrn1  30313  frgrnbnb  30321  frgrwopreglem4a  30338  2clwwlk2clwwlklem  30374  wlkl0  30395  frgrregord013  30423  frgrregord13  30424  frgrogt3nreg  30425  friendship  30427  chcompl  31270  spansncol  31596  hoaddsub  31844  bnj600  34911  sconnpht  35213  satffunlem  35385  satfvel  35396  msubvrs  35544  funpsstri  35746  imp5p  36293  cntotbnd  37782  clmgmOLD  37837  grpomndo  37861  rngoneglmul  37929  rngonegrmul  37930  zerdivemp1x  37933  atlex  39297  cvlexch1  39309  cvlsupr4  39326  cvlsupr5  39327  cvlsupr6  39328  2llnneN  39391  athgt  39438  llnle  39500  lplnle  39522  lvoli2  39563  pmaple  39743  dalawlem10  39862  dalawlem13  39865  dalawlem14  39866  dalaw  39868  lhp2lt  39983  ldilval  40095  cdleme50trn2  40533  cdlemf  40545  cdlemg18b  40661  tendotp  40743  tendospcanN  41005  dihmeetlem3N  41287  dvh4dimlem  41425  pell14qrexpclnn0  42853  pell1qrgap  42861  aomclem2  43043  rngunsnply  43157  dflim5  43318  relexpaddss  43707  rp-simp2  43782  gneispaceel2  44133  bi33imp12  44487  bi23imp13  44488  bi13imp23  44489  bi23imp1  44492  bi123imp0  44493  ee333  44504  jaoded  44563  e333  44730  suctrALTcf  44919  suctrALTcfVD  44920  ax6e2ndeqALT  44928  mullimc  45571  mullimcf  45578  f1oresf1o2  47240  fzopredsuc  47272  subsubelfzo0  47275  elsetpreimafvbi  47315  iccpartimp  47341  iccpartigtl  47347  lswn0  47368  poprelb  47448  fmtnofac1  47494  lighneallem2  47530  lighneallem3  47531  lighneallem4  47534  mogoldbblem  47644  fpprel2  47665  gbegt5  47685  sbgoldbaltlem1  47703  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  clnbgrssedg  47764  grimuhgr  47815  uhgrimisgrgriclem  47835  uhgrimisgrgric  47836  clnbgrgrim  47839  grimedg  47840  grimgrtri  47851  usgrgrtrirex  47852  isubgr3stgrlem4  47871  grlimgrtri  47898  2tceilhalfelfzo1  47952  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  gpgcubic  47969  gpg5nbgr3star  47971  lidldomn1  48074  cznnring  48105  rngccatidALTV  48115  ringccatidALTV  48149  scmsuppss  48215  lmodvsmdi  48223  gsumlsscl  48224  lindslinindimp2lem1  48303  lindsrng01  48313  elfzolborelfzop1  48364  difmodm1lt  48371  fllog2  48417  dignn0flhalflem1  48464  rrxlinesc  48584  itschlc0yqe  48609  itsclc0xyqsol  48617  itscnhlinecirc02p  48634