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  4873  wefrc  5635  iotan0  6504  f1ssf1  6835  fveqdmss  7053  funelss  8029  poxp  8110  fvn0elsuppb  8163  suppfnss  8171  smo11  8336  odi  8546  omass  8547  nndi  8590  nnmass  8591  undifixp  8910  domunfican  9279  preleqg  9575  pr2nelemOLD  9963  dfac8alem  9989  fin33i  10329  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  ttukeyg  10477  axdclem  10479  grupr  10757  nqereu  10889  squeeze0  12093  rpnnen1lem5  12947  xnn0lenn0nn0  13212  supxrun  13283  difelfzle  13609  elfzo0z  13669  fzofzim  13677  fzo1fzo0n0  13683  elfzodifsumelfzo  13699  elfznelfzo  13740  injresinj  13756  mulexp  14073  expadd  14076  expmul  14079  facdiv  14259  hashgt12el2  14395  hashimarni  14413  leisorel  14432  fi1uzind  14479  pfxfv  14654  swrdswrdlem  14676  pfxccat3  14706  reuccatpfxs1lem  14718  repswswrd  14756  cshf1  14782  2cshwcshw  14798  cshimadifsn  14802  relexpindlem  15036  pwdif  15841  dvdsaddre2b  16284  addmodlteqALT  16302  ltoddhalfle  16338  halfleoddlt  16339  coprmprod  16638  coprmproddvds  16640  cncongr1  16644  oddprmgt2  16676  prmfac1  16697  infpnlem1  16888  prmgaplem5  17033  prmgaplem6  17034  cshwshashlem1  17073  setsstruct  17153  iscatd2  17649  initoeu2lem2  17984  clatleglb  18484  dfgrp3e  18979  mulgaddcom  19037  mulginvcom  19038  symgfvne  19318  lsmcv  21058  assamulgscm  21817  psrvscafval  21864  mat1scmat  22433  cramer0  22584  chpscmat  22736  fvmptnn04ifa  22744  fvmptnn04ifc  22746  fvmptnn04ifd  22747  fiinopn  22795  opnneissb  23008  cnpimaex  23150  regsep  23228  hausnei2  23247  cmpsublem  23293  cmpsub  23294  filufint  23814  blssps  24319  blss  24320  mblsplit  25440  dvply2g  26199  taylply2  26282  bcmono  27195  gausslemma2dlem1a  27283  2sqlem10  27346  addsuniflem  27915  negsunif  27968  ssltmul2  28058  precsexlem11  28126  elntg2  28919  upgrex  29026  numedglnl  29078  ausgrumgri  29101  ausgrusgri  29102  usgredg2vtxeuALT  29156  ushgredgedg  29163  ushgredgedgloop  29165  edg0usgr  29187  0uhgrsubgr  29213  subumgredg2  29219  fusgrfisbase  29262  cusgrsizeinds  29387  cusgrsize2inds  29388  finsumvtxdg2size  29485  upgrewlkle2  29541  wlkl1loop  29573  pthdivtx  29664  2pthnloop  29668  upgrwlkdvde  29674  uhgrwkspthlem2  29691  usgr2pthlem  29700  usgr2pth  29701  clwlkl1loop  29720  crctcshwlkn0lem4  29750  wwlksnextproplem3  29848  wspn0  29861  umgr2adedgwlkonALT  29884  umgr2wlk  29886  umgr2wlkon  29887  elwwlks2  29903  clwwlkccatlem  29925  umgrclwwlkge2  29927  clwlkclwwlklem2  29936  clwlkclwwlkf1lem2  29941  clwlkclwwlkf  29944  clwwlknlbonbgr1  29975  clwwlkn1loopb  29979  clwwlkel  29982  clwwlkext2edg  29992  clwwlknonex2lem2  30044  clwwlknonex2  30045  clwwlknonex2e  30046  1pthon2v  30089  uhgr3cyclex  30118  eupth2lem3lem6  30169  frgr3vlem1  30209  3cyclfrgrrn1  30221  frgrnbnb  30229  frgrwopreglem4a  30246  2clwwlk2clwwlklem  30282  wlkl0  30303  frgrregord013  30331  frgrregord13  30332  frgrogt3nreg  30333  friendship  30335  chcompl  31178  spansncol  31504  hoaddsub  31752  bnj600  34916  sconnpht  35223  satffunlem  35395  satfvel  35406  msubvrs  35554  funpsstri  35760  imp5p  36306  cntotbnd  37797  clmgmOLD  37852  grpomndo  37876  rngoneglmul  37944  rngonegrmul  37945  zerdivemp1x  37948  atlex  39316  cvlexch1  39328  cvlsupr4  39345  cvlsupr5  39346  cvlsupr6  39347  2llnneN  39410  athgt  39457  llnle  39519  lplnle  39541  lvoli2  39582  pmaple  39762  dalawlem10  39881  dalawlem13  39884  dalawlem14  39885  dalaw  39887  lhp2lt  40002  ldilval  40114  cdleme50trn2  40552  cdlemf  40564  cdlemg18b  40680  tendotp  40762  tendospcanN  41024  dihmeetlem3N  41306  dvh4dimlem  41444  pell14qrexpclnn0  42861  pell1qrgap  42869  aomclem2  43051  rngunsnply  43165  dflim5  43325  relexpaddss  43714  rp-simp2  43789  gneispaceel2  44140  bi33imp12  44488  bi13imp23  44489  bi23imp1  44492  bi123imp0  44493  ee333  44504  jaoded  44563  e333  44729  suctrALTcf  44918  suctrALTcfVD  44919  ax6e2ndeqALT  44927  mullimc  45621  mullimcf  45628  f1oresf1o2  47296  fzopredsuc  47328  subsubelfzo0  47331  2tceilhalfelfzo1  47337  elsetpreimafvbi  47396  iccpartimp  47422  iccpartigtl  47428  lswn0  47449  poprelb  47529  fmtnofac1  47575  lighneallem2  47611  lighneallem3  47612  lighneallem4  47615  mogoldbblem  47725  fpprel2  47746  gbegt5  47766  sbgoldbaltlem1  47784  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  clnbgrssedg  47845  grimuhgr  47891  uhgrimedgi  47894  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrim  47938  grimedg  47939  grimgrtri  47952  usgrgrtrirex  47953  isubgr3stgrlem4  47972  grlimgrtri  47999  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgcubic  48074  gpg5nbgr3star  48076  lidldomn1  48223  cznnring  48254  rngccatidALTV  48264  ringccatidALTV  48298  scmsuppss  48363  lmodvsmdi  48371  gsumlsscl  48372  lindslinindimp2lem1  48451  lindsrng01  48461  elfzolborelfzop1  48512  fllog2  48561  dignn0flhalflem1  48608  rrxlinesc  48728  itschlc0yqe  48753  itsclc0xyqsol  48761  itscnhlinecirc02p  48778