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  4864  wefrc  5626  iotan0  6490  f1ssf1  6814  fveqdmss  7032  funelss  8001  poxp  8080  fvn0elsuppb  8133  suppfnss  8141  smo11  8306  odi  8516  omass  8517  nndi  8561  nnmass  8562  undifixp  8884  domunfican  9234  preleqg  9536  dfac8alem  9951  fin33i  10291  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ttukeyg  10439  axdclem  10441  grupr  10720  nqereu  10852  squeeze0  12057  rpnnen1lem5  12906  xnn0lenn0nn0  13172  supxrun  13243  difelfzle  13569  elfzo0z  13629  fzofzim  13637  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  elfznelfzo  13701  injresinj  13719  mulexp  14036  expadd  14039  expmul  14042  facdiv  14222  hashgt12el2  14358  hashimarni  14376  leisorel  14395  fi1uzind  14442  pfxfv  14618  swrdswrdlem  14639  pfxccat3  14669  reuccatpfxs1lem  14681  repswswrd  14719  cshf1  14745  2cshwcshw  14760  cshimadifsn  14764  relexpindlem  14998  pwdif  15803  dvdsaddre2b  16246  addmodlteqALT  16264  ltoddhalfle  16300  halfleoddlt  16301  coprmprod  16600  coprmproddvds  16602  cncongr1  16606  oddprmgt2  16638  prmfac1  16659  infpnlem1  16850  prmgaplem5  16995  prmgaplem6  16996  cshwshashlem1  17035  setsstruct  17115  iscatd2  17616  initoeu2lem2  17951  clatleglb  18453  dfgrp3e  18982  mulgaddcom  19040  mulginvcom  19041  symgfvne  19322  lsmcv  21108  assamulgscm  21869  psrvscafval  21916  mat1scmat  22495  cramer0  22646  chpscmat  22798  fvmptnn04ifa  22806  fvmptnn04ifc  22808  fvmptnn04ifd  22809  fiinopn  22857  opnneissb  23070  cnpimaex  23212  regsep  23290  hausnei2  23309  cmpsublem  23355  cmpsub  23356  filufint  23876  blssps  24380  blss  24381  mblsplit  25501  dvply2g  26260  taylply2  26343  bcmono  27256  gausslemma2dlem1a  27344  2sqlem10  27407  eqcuts3  27812  addsuniflem  28009  negsunif  28063  sltmuls2  28156  precsexlem11  28225  bdaypw2n0bndlem  28471  elreno2  28503  elntg2  29070  upgrex  29177  numedglnl  29229  ausgrumgri  29252  ausgrusgri  29253  usgredg2vtxeuALT  29307  ushgredgedg  29314  ushgredgedgloop  29316  edg0usgr  29338  0uhgrsubgr  29364  subumgredg2  29370  fusgrfisbase  29413  cusgrsizeinds  29538  cusgrsize2inds  29539  finsumvtxdg2size  29636  upgrewlkle2  29692  wlkl1loop  29723  pthdivtx  29812  2pthnloop  29816  upgrwlkdvde  29822  uhgrwkspthlem2  29839  usgr2pthlem  29848  usgr2pth  29849  clwlkl1loop  29868  crctcshwlkn0lem4  29898  wwlksnextproplem3  29996  wspn0  30009  umgr2adedgwlkonALT  30032  umgr2wlk  30034  umgr2wlkon  30035  elwwlks2  30054  clwwlkccatlem  30076  umgrclwwlkge2  30078  clwlkclwwlklem2  30087  clwlkclwwlkf1lem2  30092  clwlkclwwlkf  30095  clwwlknlbonbgr1  30126  clwwlkn1loopb  30130  clwwlkel  30133  clwwlkext2edg  30143  clwwlknonex2lem2  30195  clwwlknonex2  30196  clwwlknonex2e  30197  1pthon2v  30240  uhgr3cyclex  30269  eupth2lem3lem6  30320  frgr3vlem1  30360  3cyclfrgrrn1  30372  frgrnbnb  30380  frgrwopreglem4a  30397  2clwwlk2clwwlklem  30433  wlkl0  30454  frgrregord013  30482  frgrregord13  30483  frgrogt3nreg  30484  friendship  30486  chcompl  31329  spansncol  31655  hoaddsub  31903  bnj600  35094  sconnpht  35442  satffunlem  35614  satfvel  35625  msubvrs  35773  funpsstri  35979  imp5p  36524  cntotbnd  38041  clmgmOLD  38096  grpomndo  38120  rngoneglmul  38188  rngonegrmul  38189  zerdivemp1x  38192  qmapeldisjsim  39105  rnqmapeleldisjsim  39107  atlex  39686  cvlexch1  39698  cvlsupr4  39715  cvlsupr5  39716  cvlsupr6  39717  2llnneN  39779  athgt  39826  llnle  39888  lplnle  39910  lvoli2  39951  pmaple  40131  dalawlem10  40250  dalawlem13  40253  dalawlem14  40254  dalaw  40256  lhp2lt  40371  ldilval  40483  cdleme50trn2  40921  cdlemf  40933  cdlemg18b  41049  tendotp  41131  tendospcanN  41393  dihmeetlem3N  41675  dvh4dimlem  41813  pell14qrexpclnn0  43217  pell1qrgap  43225  aomclem2  43406  rngunsnply  43520  dflim5  43680  relexpaddss  44068  rp-simp2  44143  gneispaceel2  44494  bi33imp12  44841  bi13imp23  44842  bi23imp1  44845  bi123imp0  44846  ee333  44857  jaoded  44916  e333  45082  suctrALTcf  45271  suctrALTcfVD  45272  ax6e2ndeqALT  45280  mullimc  45970  mullimcf  45977  f1oresf1o2  47645  fzopredsuc  47677  subsubelfzo0  47680  2tceilhalfelfzo1  47686  elsetpreimafvbi  47745  iccpartimp  47771  iccpartigtl  47777  lswn0  47798  poprelb  47878  fmtnofac1  47924  lighneallem2  47960  lighneallem3  47961  lighneallem4  47964  mogoldbblem  48074  fpprel2  48095  gbegt5  48115  sbgoldbaltlem1  48133  bgoldbtbndlem2  48160  bgoldbtbndlem3  48161  clnbgrssedg  48195  grimuhgr  48241  uhgrimedgi  48244  uhgrimisgrgriclem  48284  uhgrimisgrgric  48285  clnbgrgrim  48288  grimedg  48289  grimgrtri  48303  usgrgrtrirex  48304  isubgr3stgrlem4  48323  grlimgrtri  48357  clnbgr3stgrgrlim  48373  gpgedgvtx1  48416  gpgvtxedg0  48417  gpgvtxedg1  48418  gpgcubic  48433  gpg5nbgr3star  48435  lidldomn1  48585  cznnring  48616  rngccatidALTV  48626  ringccatidALTV  48660  scmsuppss  48725  lmodvsmdi  48733  gsumlsscl  48734  lindslinindimp2lem1  48812  lindsrng01  48822  elfzolborelfzop1  48873  fllog2  48922  dignn0flhalflem1  48969  rrxlinesc  49089  itschlc0yqe  49114  itsclc0xyqsol  49122  itscnhlinecirc02p  49139