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  4862  wefrc  5618  iotan0  6482  f1ssf1  6806  fveqdmss  7023  funelss  7991  poxp  8070  fvn0elsuppb  8123  suppfnss  8131  smo11  8296  odi  8506  omass  8507  nndi  8551  nnmass  8552  undifixp  8872  domunfican  9222  preleqg  9524  dfac8alem  9939  fin33i  10279  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  ttukeyg  10427  axdclem  10429  grupr  10708  nqereu  10840  squeeze0  12045  rpnnen1lem5  12894  xnn0lenn0nn0  13160  supxrun  13231  difelfzle  13557  elfzo0z  13617  fzofzim  13625  fzo1fzo0n0  13631  elfzodifsumelfzo  13647  elfznelfzo  13689  injresinj  13707  mulexp  14024  expadd  14027  expmul  14030  facdiv  14210  hashgt12el2  14346  hashimarni  14364  leisorel  14383  fi1uzind  14430  pfxfv  14606  swrdswrdlem  14627  pfxccat3  14657  reuccatpfxs1lem  14669  repswswrd  14707  cshf1  14733  2cshwcshw  14748  cshimadifsn  14752  relexpindlem  14986  pwdif  15791  dvdsaddre2b  16234  addmodlteqALT  16252  ltoddhalfle  16288  halfleoddlt  16289  coprmprod  16588  coprmproddvds  16590  cncongr1  16594  oddprmgt2  16626  prmfac1  16647  infpnlem1  16838  prmgaplem5  16983  prmgaplem6  16984  cshwshashlem1  17023  setsstruct  17103  iscatd2  17604  initoeu2lem2  17939  clatleglb  18441  dfgrp3e  18970  mulgaddcom  19028  mulginvcom  19029  symgfvne  19310  lsmcv  21096  assamulgscm  21857  psrvscafval  21904  mat1scmat  22483  cramer0  22634  chpscmat  22786  fvmptnn04ifa  22794  fvmptnn04ifc  22796  fvmptnn04ifd  22797  fiinopn  22845  opnneissb  23058  cnpimaex  23200  regsep  23278  hausnei2  23297  cmpsublem  23343  cmpsub  23344  filufint  23864  blssps  24368  blss  24369  mblsplit  25489  dvply2g  26248  taylply2  26331  bcmono  27244  gausslemma2dlem1a  27332  2sqlem10  27395  eqcuts3  27800  addsuniflem  27997  negsunif  28051  sltmuls2  28144  precsexlem11  28213  bdaypw2n0bndlem  28459  elreno2  28491  elntg2  29058  upgrex  29165  numedglnl  29217  ausgrumgri  29240  ausgrusgri  29241  usgredg2vtxeuALT  29295  ushgredgedg  29302  ushgredgedgloop  29304  edg0usgr  29326  0uhgrsubgr  29352  subumgredg2  29358  fusgrfisbase  29401  cusgrsizeinds  29526  cusgrsize2inds  29527  finsumvtxdg2size  29624  upgrewlkle2  29680  wlkl1loop  29711  pthdivtx  29800  2pthnloop  29804  upgrwlkdvde  29810  uhgrwkspthlem2  29827  usgr2pthlem  29836  usgr2pth  29837  clwlkl1loop  29856  crctcshwlkn0lem4  29886  wwlksnextproplem3  29984  wspn0  29997  umgr2adedgwlkonALT  30020  umgr2wlk  30022  umgr2wlkon  30023  elwwlks2  30042  clwwlkccatlem  30064  umgrclwwlkge2  30066  clwlkclwwlklem2  30075  clwlkclwwlkf1lem2  30080  clwlkclwwlkf  30083  clwwlknlbonbgr1  30114  clwwlkn1loopb  30118  clwwlkel  30121  clwwlkext2edg  30131  clwwlknonex2lem2  30183  clwwlknonex2  30184  clwwlknonex2e  30185  1pthon2v  30228  uhgr3cyclex  30257  eupth2lem3lem6  30308  frgr3vlem1  30348  3cyclfrgrrn1  30360  frgrnbnb  30368  frgrwopreglem4a  30385  2clwwlk2clwwlklem  30421  wlkl0  30442  frgrregord013  30470  frgrregord13  30471  frgrogt3nreg  30472  friendship  30474  chcompl  31317  spansncol  31643  hoaddsub  31891  bnj600  35075  sconnpht  35423  satffunlem  35595  satfvel  35606  msubvrs  35754  funpsstri  35960  imp5p  36505  cntotbnd  37993  clmgmOLD  38048  grpomndo  38072  rngoneglmul  38140  rngonegrmul  38141  zerdivemp1x  38144  atlex  39572  cvlexch1  39584  cvlsupr4  39601  cvlsupr5  39602  cvlsupr6  39603  2llnneN  39665  athgt  39712  llnle  39774  lplnle  39796  lvoli2  39837  pmaple  40017  dalawlem10  40136  dalawlem13  40139  dalawlem14  40140  dalaw  40142  lhp2lt  40257  ldilval  40369  cdleme50trn2  40807  cdlemf  40819  cdlemg18b  40935  tendotp  41017  tendospcanN  41279  dihmeetlem3N  41561  dvh4dimlem  41699  pell14qrexpclnn0  43104  pell1qrgap  43112  aomclem2  43293  rngunsnply  43407  dflim5  43567  relexpaddss  43955  rp-simp2  44030  gneispaceel2  44381  bi33imp12  44728  bi13imp23  44729  bi23imp1  44732  bi123imp0  44733  ee333  44744  jaoded  44803  e333  44969  suctrALTcf  45158  suctrALTcfVD  45159  ax6e2ndeqALT  45167  mullimc  45858  mullimcf  45865  f1oresf1o2  47533  fzopredsuc  47565  subsubelfzo0  47568  2tceilhalfelfzo1  47574  elsetpreimafvbi  47633  iccpartimp  47659  iccpartigtl  47665  lswn0  47686  poprelb  47766  fmtnofac1  47812  lighneallem2  47848  lighneallem3  47849  lighneallem4  47852  mogoldbblem  47962  fpprel2  47983  gbegt5  48003  sbgoldbaltlem1  48021  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  clnbgrssedg  48083  grimuhgr  48129  uhgrimedgi  48132  uhgrimisgrgriclem  48172  uhgrimisgrgric  48173  clnbgrgrim  48176  grimedg  48177  grimgrtri  48191  usgrgrtrirex  48192  isubgr3stgrlem4  48211  grlimgrtri  48245  clnbgr3stgrgrlim  48261  gpgedgvtx1  48304  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgcubic  48321  gpg5nbgr3star  48323  lidldomn1  48473  cznnring  48504  rngccatidALTV  48514  ringccatidALTV  48548  scmsuppss  48613  lmodvsmdi  48621  gsumlsscl  48622  lindslinindimp2lem1  48700  lindsrng01  48710  elfzolborelfzop1  48761  fllog2  48810  dignn0flhalflem1  48857  rrxlinesc  48977  itschlc0yqe  49002  itsclc0xyqsol  49010  itscnhlinecirc02p  49027