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 418	. 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3imp31  1112  3imp231  1113  3impb  1115  3impib  1116  3imp1  1347  3impd  1348  3jao  1425  biimp3ar  1470  3elpr2eq  4869  wefrc  5632  iotan0  6491  f1ssf1  6821  fveqdmss  7034  funelss  7984  poxp  8065  fvn0elsuppb  8117  suppfnss  8125  smo11  8315  odi  8531  omass  8532  nndi  8575  nnmass  8576  undifixp  8879  domunfican  9271  preleqg  9560  pr2nelemOLD  9948  dfac8alem  9974  fin33i  10314  domtriomlem  10387  axdc3lem2  10396  axdc3lem4  10398  axdc4lem  10400  ttukeyg  10462  axdclem  10464  grupr  10742  nqereu  10874  squeeze0  12067  rpnnen1lem5  12915  xnn0lenn0nn0  13174  supxrun  13245  difelfzle  13564  elfzo0z  13624  fzofzim  13629  fzo1fzo0n0  13633  elfzodifsumelfzo  13648  elfznelfzo  13687  injresinj  13703  mulexp  14017  expadd  14020  expmul  14023  facdiv  14197  hashgt12el2  14333  hashimarni  14351  leisorel  14371  fi1uzind  14408  pfxfv  14582  swrdswrdlem  14604  pfxccat3  14634  reuccatpfxs1lem  14646  repswswrd  14684  cshf1  14710  2cshwcshw  14726  cshimadifsn  14730  relexpindlem  14960  pwdif  15764  dvdsaddre2b  16200  addmodlteqALT  16218  ltoddhalfle  16254  halfleoddlt  16255  coprmprod  16548  coprmproddvds  16550  cncongr1  16554  oddprmgt2  16586  prmfac1  16608  infpnlem1  16793  prmgaplem5  16938  prmgaplem6  16939  cshwshashlem1  16979  setsstruct  17059  iscatd2  17575  initoeu2lem2  17915  clatleglb  18421  dfgrp3e  18861  mulgaddcom  18914  mulginvcom  18915  symgfvne  19176  f1rhm0to0ALT  20191  lsmcv  20661  assamulgscm  21341  psrvscafval  21395  mat1scmat  21925  cramer0  22076  chpscmat  22228  fvmptnn04ifa  22236  fvmptnn04ifc  22238  fvmptnn04ifd  22239  fiinopn  22287  opnneissb  22502  cnpimaex  22644  regsep  22722  hausnei2  22741  cmpsublem  22787  cmpsub  22788  filufint  23308  blssps  23814  blss  23815  mblsplit  24933  bcmono  26662  gausslemma2dlem1a  26750  2sqlem10  26813  addsunif  27353  negsunif  27393  elntg2  27997  upgrex  28106  numedglnl  28158  ausgrumgri  28181  ausgrusgri  28182  usgredg2vtxeuALT  28233  ushgredgedg  28240  ushgredgedgloop  28242  edg0usgr  28264  0uhgrsubgr  28290  subumgredg2  28296  fusgrfisbase  28339  cusgrsizeinds  28463  cusgrsize2inds  28464  finsumvtxdg2size  28561  upgrewlkle2  28617  wlkl1loop  28649  pthdivtx  28740  2pthnloop  28742  upgrwlkdvde  28748  uhgrwkspthlem2  28765  usgr2pthlem  28774  usgr2pth  28775  clwlkl1loop  28794  crctcshwlkn0lem4  28821  wwlksnextproplem3  28919  wspn0  28932  umgr2adedgwlkonALT  28955  umgr2wlk  28957  umgr2wlkon  28958  elwwlks2  28974  clwwlkccatlem  28996  umgrclwwlkge2  28998  clwlkclwwlklem2  29007  clwlkclwwlkf1lem2  29012  clwlkclwwlkf  29015  clwwlknlbonbgr1  29046  clwwlkn1loopb  29050  clwwlkel  29053  clwwlkext2edg  29063  clwwlknonex2lem2  29115  clwwlknonex2  29116  clwwlknonex2e  29117  1pthon2v  29160  uhgr3cyclex  29189  eupth2lem3lem6  29240  frgr3vlem1  29280  3cyclfrgrrn1  29292  frgrnbnb  29300  frgrwopreglem4a  29317  2clwwlk2clwwlklem  29353  wlkl0  29374  frgrregord013  29402  frgrregord13  29403  frgrogt3nreg  29404  friendship  29406  chcompl  30247  spansncol  30573  hoaddsub  30821  bnj600  33620  sconnpht  33910  satffunlem  34082  satfvel  34093  msubvrs  34241  funpsstri  34426  imp5p  34859  cntotbnd  36328  clmgmOLD  36383  grpomndo  36407  rngoneglmul  36475  rngonegrmul  36476  zerdivemp1x  36479  atlex  37851  cvlexch1  37863  cvlsupr4  37880  cvlsupr5  37881  cvlsupr6  37882  2llnneN  37945  athgt  37992  llnle  38054  lplnle  38076  lvoli2  38117  pmaple  38297  dalawlem10  38416  dalawlem13  38419  dalawlem14  38420  dalaw  38422  lhp2lt  38537  ldilval  38649  cdleme50trn2  39087  cdlemf  39099  cdlemg18b  39215  tendotp  39297  tendospcanN  39559  dihmeetlem3N  39841  dvh4dimlem  39979  pell14qrexpclnn0  41247  pell1qrgap  41255  aomclem2  41440  rngunsnply  41558  dflim5  41722  relexpaddss  42112  rp-simp2  42187  gneispaceel2  42538  bi33imp12  42894  bi23imp13  42895  bi13imp23  42896  bi23imp1  42899  bi123imp0  42900  ee333  42911  jaoded  42970  e333  43137  suctrALTcf  43326  suctrALTcfVD  43327  ax6e2ndeqALT  43335  mullimc  43977  mullimcf  43984  f1oresf1o2  45643  fzopredsuc  45675  subsubelfzo0  45678  elsetpreimafvbi  45703  iccpartimp  45729  iccpartigtl  45735  lswn0  45756  poprelb  45836  fmtnofac1  45882  lighneallem2  45918  lighneallem3  45919  lighneallem4  45922  mogoldbblem  46032  fpprel2  46053  gbegt5  46073  sbgoldbaltlem1  46091  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  lidldomn1  46339  cznnring  46374  rngccatidALTV  46407  ringccatidALTV  46470  scmsuppss  46568  lmodvsmdi  46578  gsumlsscl  46579  lindslinindimp2lem1  46659  lindsrng01  46669  elfzolborelfzop1  46720  difmodm1lt  46728  fllog2  46774  dignn0flhalflem1  46821  rrxlinesc  46941  itschlc0yqe  46966  itsclc0xyqsol  46974  itscnhlinecirc02p  46991