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  4882  wefrc  5648  iotan0  6520  f1ssf1  6849  fveqdmss  7067  funelss  8044  poxp  8125  fvn0elsuppb  8178  suppfnss  8186  smo11  8376  odi  8589  omass  8590  nndi  8633  nnmass  8634  undifixp  8946  domunfican  9331  preleqg  9627  pr2nelemOLD  10015  dfac8alem  10041  fin33i  10381  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  ttukeyg  10529  axdclem  10531  grupr  10809  nqereu  10941  squeeze0  12143  rpnnen1lem5  12995  xnn0lenn0nn0  13259  supxrun  13330  difelfzle  13656  elfzo0z  13716  fzofzim  13724  fzo1fzo0n0  13729  elfzodifsumelfzo  13745  elfznelfzo  13786  injresinj  13802  mulexp  14117  expadd  14120  expmul  14123  facdiv  14303  hashgt12el2  14439  hashimarni  14457  leisorel  14476  fi1uzind  14523  pfxfv  14698  swrdswrdlem  14720  pfxccat3  14750  reuccatpfxs1lem  14762  repswswrd  14800  cshf1  14826  2cshwcshw  14842  cshimadifsn  14846  relexpindlem  15080  pwdif  15882  dvdsaddre2b  16324  addmodlteqALT  16342  ltoddhalfle  16378  halfleoddlt  16379  coprmprod  16678  coprmproddvds  16680  cncongr1  16684  oddprmgt2  16716  prmfac1  16737  infpnlem1  16928  prmgaplem5  17073  prmgaplem6  17074  cshwshashlem1  17113  setsstruct  17193  iscatd2  17691  initoeu2lem2  18026  clatleglb  18526  dfgrp3e  19021  mulgaddcom  19079  mulginvcom  19080  symgfvne  19360  lsmcv  21100  assamulgscm  21859  psrvscafval  21906  mat1scmat  22475  cramer0  22626  chpscmat  22778  fvmptnn04ifa  22786  fvmptnn04ifc  22788  fvmptnn04ifd  22789  fiinopn  22837  opnneissb  23050  cnpimaex  23192  regsep  23270  hausnei2  23289  cmpsublem  23335  cmpsub  23336  filufint  23856  blssps  24361  blss  24362  mblsplit  25483  dvply2g  26242  taylply2  26325  bcmono  27238  gausslemma2dlem1a  27326  2sqlem10  27389  addsuniflem  27951  negsunif  28004  ssltmul2  28091  precsexlem11  28158  elntg2  28910  upgrex  29017  numedglnl  29069  ausgrumgri  29092  ausgrusgri  29093  usgredg2vtxeuALT  29147  ushgredgedg  29154  ushgredgedgloop  29156  edg0usgr  29178  0uhgrsubgr  29204  subumgredg2  29210  fusgrfisbase  29253  cusgrsizeinds  29378  cusgrsize2inds  29379  finsumvtxdg2size  29476  upgrewlkle2  29532  wlkl1loop  29564  pthdivtx  29655  2pthnloop  29659  upgrwlkdvde  29665  uhgrwkspthlem2  29682  usgr2pthlem  29691  usgr2pth  29692  clwlkl1loop  29711  crctcshwlkn0lem4  29741  wwlksnextproplem3  29839  wspn0  29852  umgr2adedgwlkonALT  29875  umgr2wlk  29877  umgr2wlkon  29878  elwwlks2  29894  clwwlkccatlem  29916  umgrclwwlkge2  29918  clwlkclwwlklem2  29927  clwlkclwwlkf1lem2  29932  clwlkclwwlkf  29935  clwwlknlbonbgr1  29966  clwwlkn1loopb  29970  clwwlkel  29973  clwwlkext2edg  29983  clwwlknonex2lem2  30035  clwwlknonex2  30036  clwwlknonex2e  30037  1pthon2v  30080  uhgr3cyclex  30109  eupth2lem3lem6  30160  frgr3vlem1  30200  3cyclfrgrrn1  30212  frgrnbnb  30220  frgrwopreglem4a  30237  2clwwlk2clwwlklem  30273  wlkl0  30294  frgrregord013  30322  frgrregord13  30323  frgrogt3nreg  30324  friendship  30326  chcompl  31169  spansncol  31495  hoaddsub  31743  bnj600  34896  sconnpht  35197  satffunlem  35369  satfvel  35380  msubvrs  35528  funpsstri  35729  imp5p  36275  cntotbnd  37766  clmgmOLD  37821  grpomndo  37845  rngoneglmul  37913  rngonegrmul  37914  zerdivemp1x  37917  atlex  39280  cvlexch1  39292  cvlsupr4  39309  cvlsupr5  39310  cvlsupr6  39311  2llnneN  39374  athgt  39421  llnle  39483  lplnle  39505  lvoli2  39546  pmaple  39726  dalawlem10  39845  dalawlem13  39848  dalawlem14  39849  dalaw  39851  lhp2lt  39966  ldilval  40078  cdleme50trn2  40516  cdlemf  40528  cdlemg18b  40644  tendotp  40726  tendospcanN  40988  dihmeetlem3N  41270  dvh4dimlem  41408  pell14qrexpclnn0  42836  pell1qrgap  42844  aomclem2  43026  rngunsnply  43140  dflim5  43300  relexpaddss  43689  rp-simp2  43764  gneispaceel2  44115  bi33imp12  44464  bi13imp23  44465  bi23imp1  44468  bi123imp0  44469  ee333  44480  jaoded  44539  e333  44705  suctrALTcf  44894  suctrALTcfVD  44895  ax6e2ndeqALT  44903  mullimc  45593  mullimcf  45600  f1oresf1o2  47268  fzopredsuc  47300  subsubelfzo0  47303  2tceilhalfelfzo1  47309  elsetpreimafvbi  47353  iccpartimp  47379  iccpartigtl  47385  lswn0  47406  poprelb  47486  fmtnofac1  47532  lighneallem2  47568  lighneallem3  47569  lighneallem4  47572  mogoldbblem  47682  fpprel2  47703  gbegt5  47723  sbgoldbaltlem1  47741  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  clnbgrssedg  47802  grimuhgr  47848  uhgrimedgi  47851  uhgrimisgrgriclem  47891  uhgrimisgrgric  47892  clnbgrgrim  47895  grimedg  47896  grimgrtri  47909  usgrgrtrirex  47910  isubgr3stgrlem4  47929  grlimgrtri  47956  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  gpgcubic  48029  gpg5nbgr3star  48031  lidldomn1  48154  cznnring  48185  rngccatidALTV  48195  ringccatidALTV  48229  scmsuppss  48294  lmodvsmdi  48302  gsumlsscl  48303  lindslinindimp2lem1  48382  lindsrng01  48392  elfzolborelfzop1  48443  difmodm1lt  48450  fllog2  48496  dignn0flhalflem1  48543  rrxlinesc  48663  itschlc0yqe  48688  itsclc0xyqsol  48696  itscnhlinecirc02p  48713