Theorem 3imp 1128

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 423	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3imp31  1129  3imp231  1130  3impb  1132  bi23imp13  1133  3impib  1134  3imp1  1366  3impd  1367  3jao  1452  biimp3ar  1499  3elpr2eq  4833  wefrc  5644  iotan0  6528  f1ssf1  6857  fveqdmss  7078  funelss  8058  poxp  8142  fvn0elsuppb  8201  suppfnss  8209  smo11  8375  odi  8590  omass  8591  nndi  8635  nnmass  8636  undifixp  8965  domunfican  9316  preleqg  9619  dfac8alem  10111  fin33i  10450  domtriomlem  10523  axdc3lem2  10532  axdc3lem4  10534  axdc4lem  10536  ttukeyg  10598  axdclem  10600  grupr  10885  nqereu  11017  squeeze0  12223  rpnnen1lem5  13112  xnn0lenn0nn0  13378  supxrun  13449  difelfzle  13778  elfzo0z  13839  fzofzim  13847  fzo1fzo0n0  13853  elfzodifsumelfzo  13869  elfznelfzo  13911  injresinj  13929  mulexp  14247  expadd  14250  expmul  14253  facdiv  14434  hashgt12el2  14571  hashimarni  14589  leisorel  14608  fi1uzind  14655  pfxfv  14836  swrdswrdlem  14857  pfxccat3  14887  reuccatpfxs1lem  14899  repswswrd  14939  cshf1  14965  2cshwcshw  14980  cshimadifsn  14984  relexpindlem  15221  pwdif  16042  dvdsaddre2b  16482  addmodlteqALT  16500  ltoddhalfle  16536  halfleoddlt  16537  coprmprod  16841  coprmproddvds  16843  cncongr1  16847  oddprmgt2  16880  prmfac1  16901  infpnlem1  17093  prmgaplem5  17238  prmgaplem6  17239  cshwshashlem1  17278  setsstruct  17359  iscatd2  17860  initoeu2lem2  18195  clatleglb  18697  dfgrp3e  19255  mulgaddcom  19313  mulginvcom  19314  symgfvne  19600  isdrng3lem2  21011  lsmcv  21424  lidlunin0  21520  assamulgscm  22214  psrvscafval  22261  mat1scmat  22859  cramer0  23013  chpscmat  23165  fvmptnn04ifa  23173  fvmptnn04ifc  23175  fvmptnn04ifd  23176  fiinopn  23224  opnneissb  23437  cnpimaex  23579  regsep  23657  hausnei2  23676  cmpsublem  23722  cmpsub  23723  filufint  24244  blssps  24748  blss  24749  mblsplit  25858  dvply2g  26611  taylply2  26700  bcmono  27609  gausslemma2dlem1a  27697  2sqlem10  27760  fltoprmlem2  27999  eqcuts3  28195  addsuniflem  28392  negsunif  28446  sltmuls2  28539  precsexlem11  28608  bdaypw2n0bndlem  28854  elreno2  28886  elntg2  29568  upgrex  29675  numedglnl  29727  ausgrumgri  29753  ausgrusgri  29754  usgredg2vtxeuALT  29808  ushgredgedg  29815  ushgredgedgloop  29817  edg0usgr  29839  0uhgrsubgr  29865  subumgredg2  29871  fusgrfisbase  29914  cusgrsizeinds  30038  cusgrsize2inds  30039  finsumvtxdg2size  30136  upgrewlkle2  30192  wlkl1loop  30223  pthdivtx  30317  2pthnloop  30322  upgrwlkdvde  30328  uhgrwkspthlem2  30345  usgr2pthlem  30354  usgr2pth  30355  clwlkl1loop  30375  crctcshwlkn0lem4  30407  wwlksnextproplem3  30505  wspn0  30518  umgr2adedgwlkonALT  30541  umgr2wlk  30543  umgr2wlkon  30544  elwwlks2  30563  clwwlkccatlem  30585  umgrclwwlkge2  30587  clwlkclwwlklem2  30596  clwlkclwwlkf1lem2  30601  clwlkclwwlkf  30604  clwwlknlbonbgr1  30635  clwwlkn1loopb  30639  clwwlkel  30642  clwwlkext2edg  30652  clwwlknonex2lem2  30704  clwwlknonex2  30705  clwwlknonex2e  30706  1pthon2v  30759  uhgr3cyclex  30788  eupth2lem3lem6  30839  frgr3vlem1  30879  3cyclfrgrrn1  30891  frgrnbnb  30899  frgrwopreglem4a  30916  2clwwlk2clwwlklem  30952  wlkl0  30973  frgrregord013  31001  frgrregord13  31002  frgrogt3nreg  31003  friendship  31005  chcompl  31849  spansncol  32175  hoaddsub  32423  bnj600  35595  sconnpht  36080  satffunlem  36252  satfvel  36263  msubvrs  36411  funpsstri  36623  imp5p  37192  cntotbnd  38823  clmgmOLD  38878  grpomndo  38902  rngoneglmul  38970  rngonegrmul  38971  zerdivemp1x  38974  qmapeldisjsim  39885  rnqmapeleldisjsim  39887  atlex  40466  cvlexch1  40478  cvlsupr4  40495  cvlsupr5  40496  cvlsupr6  40497  2llnneN  40559  athgt  40606  llnle  40668  lplnle  40690  lvoli2  40731  pmaple  40911  dalawlem10  41030  dalawlem13  41033  dalawlem14  41034  dalaw  41036  lhp2lt  41151  ldilval  41263  cdleme50trn2  41701  cdlemf  41713  cdlemg18b  41829  tendotp  41911  tendospcanN  42173  dihmeetlem3N  42455  dvh4dimlem  42593  pell14qrexpclnn0  43966  pell1qrgap  43974  aomclem2  44150  rngunsnply  44264  dflim5  44424  relexpaddss  44811  rp-simp2  44886  gneispaceel2  45237  bi33imp12  45567  bi13imp23  45568  bi23imp1  45571  bi123imp0  45572  ee333  45583  jaoded  45642  e333  45808  suctrALTcf  45997  suctrALTcfVD  45998  ax6e2ndeqALT  46006  mullimc  46721  mullimcf  46728  f1oresf1o2  48454  fzopredsuc  48487  subsubelfzo0  48490  nnmul2b  48494  2tceilhalfelfzo1  48499  2timesltsqm1  48542  muldvdsfacgt  48549  muldvdsfacm1  48550  elsetpreimafvbi  48566  iccpartimp  48592  iccpartigtl  48598  lswn0  48619  poprelb  48699  fmtnofac1  48748  lighneallem2  48784  lighneallem3  48785  lighneallem4  48788  nprmdvdsfacm1lem2  48799  mogoldbblem  48911  fpprel2  48932  gbegt5  48952  sbgoldbaltlem1  48970  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  clnbgrssedg  49032  grimuhgr  49078  uhgrimedgi  49081  uhgrimisgrgriclem  49121  uhgrimisgrgric  49122  clnbgrgrim  49125  grimedg  49126  grimgrtri  49140  usgrgrtrirex  49141  isubgr3stgrlem4  49160  grlimgrtri  49194  clnbgr3stgrgrlim  49210  gpgedgvtx1  49253  gpgvtxedg0  49254  gpgvtxedg1  49255  gpgcubic  49270  gpg5nbgr3star  49272  lidldomn1  49421  cznnring  49452  rngccatidALTV  49462  ringccatidALTV  49496  scmsuppss  49576  lmodvsmdi  49584  gsumlsscl  49585  lindslinindimp2lem1  49663  lindsrng01  49673  elfzolborelfzop1  49724  fllog2  49773  dignn0flhalflem1  49820  rrxlinesc  49941  itschlc0yqe  49965  itsclc0xyqsol  49973