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  4870  wefrc  5632  iotan0  6501  f1ssf1  6832  fveqdmss  7050  funelss  8026  poxp  8107  fvn0elsuppb  8160  suppfnss  8168  smo11  8333  odi  8543  omass  8544  nndi  8587  nnmass  8588  undifixp  8907  domunfican  9272  preleqg  9568  pr2nelemOLD  9956  dfac8alem  9982  fin33i  10322  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  ttukeyg  10470  axdclem  10472  grupr  10750  nqereu  10882  squeeze0  12086  rpnnen1lem5  12940  xnn0lenn0nn0  13205  supxrun  13276  difelfzle  13602  elfzo0z  13662  fzofzim  13670  fzo1fzo0n0  13676  elfzodifsumelfzo  13692  elfznelfzo  13733  injresinj  13749  mulexp  14066  expadd  14069  expmul  14072  facdiv  14252  hashgt12el2  14388  hashimarni  14406  leisorel  14425  fi1uzind  14472  pfxfv  14647  swrdswrdlem  14669  pfxccat3  14699  reuccatpfxs1lem  14711  repswswrd  14749  cshf1  14775  2cshwcshw  14791  cshimadifsn  14795  relexpindlem  15029  pwdif  15834  dvdsaddre2b  16277  addmodlteqALT  16295  ltoddhalfle  16331  halfleoddlt  16332  coprmprod  16631  coprmproddvds  16633  cncongr1  16637  oddprmgt2  16669  prmfac1  16690  infpnlem1  16881  prmgaplem5  17026  prmgaplem6  17027  cshwshashlem1  17066  setsstruct  17146  iscatd2  17642  initoeu2lem2  17977  clatleglb  18477  dfgrp3e  18972  mulgaddcom  19030  mulginvcom  19031  symgfvne  19311  lsmcv  21051  assamulgscm  21810  psrvscafval  21857  mat1scmat  22426  cramer0  22577  chpscmat  22729  fvmptnn04ifa  22737  fvmptnn04ifc  22739  fvmptnn04ifd  22740  fiinopn  22788  opnneissb  23001  cnpimaex  23143  regsep  23221  hausnei2  23240  cmpsublem  23286  cmpsub  23287  filufint  23807  blssps  24312  blss  24313  mblsplit  25433  dvply2g  26192  taylply2  26275  bcmono  27188  gausslemma2dlem1a  27276  2sqlem10  27339  addsuniflem  27908  negsunif  27961  ssltmul2  28051  precsexlem11  28119  elntg2  28912  upgrex  29019  numedglnl  29071  ausgrumgri  29094  ausgrusgri  29095  usgredg2vtxeuALT  29149  ushgredgedg  29156  ushgredgedgloop  29158  edg0usgr  29180  0uhgrsubgr  29206  subumgredg2  29212  fusgrfisbase  29255  cusgrsizeinds  29380  cusgrsize2inds  29381  finsumvtxdg2size  29478  upgrewlkle2  29534  wlkl1loop  29566  pthdivtx  29657  2pthnloop  29661  upgrwlkdvde  29667  uhgrwkspthlem2  29684  usgr2pthlem  29693  usgr2pth  29694  clwlkl1loop  29713  crctcshwlkn0lem4  29743  wwlksnextproplem3  29841  wspn0  29854  umgr2adedgwlkonALT  29877  umgr2wlk  29879  umgr2wlkon  29880  elwwlks2  29896  clwwlkccatlem  29918  umgrclwwlkge2  29920  clwlkclwwlklem2  29929  clwlkclwwlkf1lem2  29934  clwlkclwwlkf  29937  clwwlknlbonbgr1  29968  clwwlkn1loopb  29972  clwwlkel  29975  clwwlkext2edg  29985  clwwlknonex2lem2  30037  clwwlknonex2  30038  clwwlknonex2e  30039  1pthon2v  30082  uhgr3cyclex  30111  eupth2lem3lem6  30162  frgr3vlem1  30202  3cyclfrgrrn1  30214  frgrnbnb  30222  frgrwopreglem4a  30239  2clwwlk2clwwlklem  30275  wlkl0  30296  frgrregord013  30324  frgrregord13  30325  frgrogt3nreg  30326  friendship  30328  chcompl  31171  spansncol  31497  hoaddsub  31745  bnj600  34909  sconnpht  35216  satffunlem  35388  satfvel  35399  msubvrs  35547  funpsstri  35753  imp5p  36299  cntotbnd  37790  clmgmOLD  37845  grpomndo  37869  rngoneglmul  37937  rngonegrmul  37938  zerdivemp1x  37941  atlex  39309  cvlexch1  39321  cvlsupr4  39338  cvlsupr5  39339  cvlsupr6  39340  2llnneN  39403  athgt  39450  llnle  39512  lplnle  39534  lvoli2  39575  pmaple  39755  dalawlem10  39874  dalawlem13  39877  dalawlem14  39878  dalaw  39880  lhp2lt  39995  ldilval  40107  cdleme50trn2  40545  cdlemf  40557  cdlemg18b  40673  tendotp  40755  tendospcanN  41017  dihmeetlem3N  41299  dvh4dimlem  41437  pell14qrexpclnn0  42854  pell1qrgap  42862  aomclem2  43044  rngunsnply  43158  dflim5  43318  relexpaddss  43707  rp-simp2  43782  gneispaceel2  44133  bi33imp12  44481  bi13imp23  44482  bi23imp1  44485  bi123imp0  44486  ee333  44497  jaoded  44556  e333  44722  suctrALTcf  44911  suctrALTcfVD  44912  ax6e2ndeqALT  44920  mullimc  45614  mullimcf  45621  f1oresf1o2  47292  fzopredsuc  47324  subsubelfzo0  47327  2tceilhalfelfzo1  47333  elsetpreimafvbi  47392  iccpartimp  47418  iccpartigtl  47424  lswn0  47445  poprelb  47525  fmtnofac1  47571  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  mogoldbblem  47721  fpprel2  47742  gbegt5  47762  sbgoldbaltlem1  47780  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  clnbgrssedg  47841  grimuhgr  47887  uhgrimedgi  47890  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrim  47934  grimedg  47935  grimgrtri  47948  usgrgrtrirex  47949  isubgr3stgrlem4  47968  grlimgrtri  47995  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgcubic  48070  gpg5nbgr3star  48072  lidldomn1  48219  cznnring  48250  rngccatidALTV  48260  ringccatidALTV  48294  scmsuppss  48359  lmodvsmdi  48367  gsumlsscl  48368  lindslinindimp2lem1  48447  lindsrng01  48457  elfzolborelfzop1  48508  fllog2  48557  dignn0flhalflem1  48604  rrxlinesc  48724  itschlc0yqe  48749  itsclc0xyqsol  48757  itscnhlinecirc02p  48774