Theorem 3imp 1128

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 423	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3imp31  1129  3imp231  1130  3impb  1132  bi23imp13  1133  3impib  1134  3imp1  1366  3impd  1367  3jao  1452  biimp3ar  1499  3elpr2eq  4866  wefrc  5645  iotan0  6521  f1ssf1  6849  fveqdmss  7070  funelss  8047  poxp  8129  fvn0elsuppb  8182  suppfnss  8190  smo11  8356  odi  8571  omass  8572  nndi  8616  nnmass  8617  undifixp  8946  domunfican  9297  preleqg  9600  dfac8alem  10089  fin33i  10428  domtriomlem  10501  axdc3lem2  10510  axdc3lem4  10512  axdc4lem  10514  ttukeyg  10576  axdclem  10578  grupr  10863  nqereu  10995  squeeze0  12201  rpnnen1lem5  13090  xnn0lenn0nn0  13356  supxrun  13427  difelfzle  13755  elfzo0z  13816  fzofzim  13824  fzo1fzo0n0  13830  elfzodifsumelfzo  13846  elfznelfzo  13888  injresinj  13906  mulexp  14224  expadd  14227  expmul  14230  facdiv  14411  hashgt12el2  14548  hashimarni  14566  leisorel  14585  fi1uzind  14632  pfxfv  14812  swrdswrdlem  14833  pfxccat3  14863  reuccatpfxs1lem  14875  repswswrd  14915  cshf1  14941  2cshwcshw  14956  cshimadifsn  14960  relexpindlem  15196  pwdif  16017  dvdsaddre2b  16457  addmodlteqALT  16475  ltoddhalfle  16511  halfleoddlt  16512  coprmprod  16816  coprmproddvds  16818  cncongr1  16822  oddprmgt2  16855  prmfac1  16876  infpnlem1  17068  prmgaplem5  17213  prmgaplem6  17214  cshwshashlem1  17253  setsstruct  17334  iscatd2  17835  initoeu2lem2  18170  clatleglb  18672  dfgrp3e  19230  mulgaddcom  19288  mulginvcom  19289  symgfvne  19575  isdrng3lem2  20986  lsmcv  21399  lidlunin0  21495  assamulgscm  22189  psrvscafval  22236  mat1scmat  22834  cramer0  22988  chpscmat  23140  fvmptnn04ifa  23148  fvmptnn04ifc  23150  fvmptnn04ifd  23151  fiinopn  23199  opnneissb  23412  cnpimaex  23554  regsep  23632  hausnei2  23651  cmpsublem  23697  cmpsub  23698  filufint  24219  blssps  24723  blss  24724  mblsplit  25833  dvply2g  26588  taylply2  26677  bcmono  27586  gausslemma2dlem1a  27674  2sqlem10  27737  fltoprmlem2  27976  eqcuts3  28172  addsuniflem  28369  negsunif  28423  sltmuls2  28516  precsexlem11  28585  bdaypw2n0bndlem  28831  elreno2  28863  elntg2  29545  upgrex  29652  numedglnl  29704  ausgrumgri  29730  ausgrusgri  29731  usgredg2vtxeuALT  29785  ushgredgedg  29792  ushgredgedgloop  29794  edg0usgr  29816  0uhgrsubgr  29842  subumgredg2  29848  fusgrfisbase  29891  cusgrsizeinds  30015  cusgrsize2inds  30016  finsumvtxdg2size  30113  upgrewlkle2  30169  wlkl1loop  30200  pthdivtx  30294  2pthnloop  30299  upgrwlkdvde  30305  uhgrwkspthlem2  30322  usgr2pthlem  30331  usgr2pth  30332  clwlkl1loop  30352  crctcshwlkn0lem4  30384  wwlksnextproplem3  30482  wspn0  30495  umgr2adedgwlkonALT  30518  umgr2wlk  30520  umgr2wlkon  30521  elwwlks2  30540  clwwlkccatlem  30562  umgrclwwlkge2  30564  clwlkclwwlklem2  30573  clwlkclwwlkf1lem2  30578  clwlkclwwlkf  30581  clwwlknlbonbgr1  30612  clwwlkn1loopb  30616  clwwlkel  30619  clwwlkext2edg  30629  clwwlknonex2lem2  30681  clwwlknonex2  30682  clwwlknonex2e  30683  1pthon2v  30736  uhgr3cyclex  30765  eupth2lem3lem6  30816  frgr3vlem1  30856  3cyclfrgrrn1  30868  frgrnbnb  30876  frgrwopreglem4a  30893  2clwwlk2clwwlklem  30929  wlkl0  30950  frgrregord013  30978  frgrregord13  30979  frgrogt3nreg  30980  friendship  30982  chcompl  31826  spansncol  32152  hoaddsub  32400  bnj600  35532  sconnpht  35963  satffunlem  36135  satfvel  36146  msubvrs  36294  funpsstri  36500  imp5p  37070  cntotbnd  38698  clmgmOLD  38753  grpomndo  38777  rngoneglmul  38845  rngonegrmul  38846  zerdivemp1x  38849  qmapeldisjsim  39760  rnqmapeleldisjsim  39762  atlex  40341  cvlexch1  40353  cvlsupr4  40370  cvlsupr5  40371  cvlsupr6  40372  2llnneN  40434  athgt  40481  llnle  40543  lplnle  40565  lvoli2  40606  pmaple  40786  dalawlem10  40905  dalawlem13  40908  dalawlem14  40909  dalaw  40911  lhp2lt  41026  ldilval  41138  cdleme50trn2  41576  cdlemf  41588  cdlemg18b  41704  tendotp  41786  tendospcanN  42048  dihmeetlem3N  42330  dvh4dimlem  42468  pell14qrexpclnn0  43826  pell1qrgap  43834  aomclem2  44015  rngunsnply  44129  dflim5  44289  relexpaddss  44677  rp-simp2  44752  gneispaceel2  45103  bi33imp12  45433  bi13imp23  45434  bi23imp1  45437  bi123imp0  45438  ee333  45449  jaoded  45508  e333  45674  suctrALTcf  45863  suctrALTcfVD  45864  ax6e2ndeqALT  45872  mullimc  46572  mullimcf  46579  f1oresf1o2  48305  fzopredsuc  48338  subsubelfzo0  48341  nnmul2b  48345  2tceilhalfelfzo1  48350  2timesltsqm1  48393  muldvdsfacgt  48400  muldvdsfacm1  48401  elsetpreimafvbi  48417  iccpartimp  48443  iccpartigtl  48449  lswn0  48470  poprelb  48550  fmtnofac1  48599  lighneallem2  48635  lighneallem3  48636  lighneallem4  48639  nprmdvdsfacm1lem2  48650  mogoldbblem  48762  fpprel2  48783  gbegt5  48803  sbgoldbaltlem1  48821  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  clnbgrssedg  48883  grimuhgr  48929  uhgrimedgi  48932  uhgrimisgrgriclem  48972  uhgrimisgrgric  48973  clnbgrgrim  48976  grimedg  48977  grimgrtri  48991  usgrgrtrirex  48992  isubgr3stgrlem4  49011  grlimgrtri  49045  clnbgr3stgrgrlim  49061  gpgedgvtx1  49104  gpgvtxedg0  49105  gpgvtxedg1  49106  gpgcubic  49121  gpg5nbgr3star  49123  lidldomn1  49272  cznnring  49303  rngccatidALTV  49313  ringccatidALTV  49347  scmsuppss  49427  lmodvsmdi  49435  gsumlsscl  49436  lindslinindimp2lem1  49514  lindsrng01  49524  elfzolborelfzop1  49575  fllog2  49624  dignn0flhalflem1  49671  rrxlinesc  49791  itschlc0yqe  49816  itsclc0xyqsol  49824  itscnhlinecirc02p  49841