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  4857  wefrc  5613  iotan0  6476  f1ssf1  6800  fveqdmss  7017  funelss  7985  poxp  8064  fvn0elsuppb  8117  suppfnss  8125  smo11  8290  odi  8500  omass  8501  nndi  8544  nnmass  8545  undifixp  8864  domunfican  9213  preleqg  9512  dfac8alem  9927  fin33i  10267  domtriomlem  10340  axdc3lem2  10349  axdc3lem4  10351  axdc4lem  10353  ttukeyg  10415  axdclem  10417  grupr  10695  nqereu  10827  squeeze0  12032  rpnnen1lem5  12881  xnn0lenn0nn0  13146  supxrun  13217  difelfzle  13543  elfzo0z  13603  fzofzim  13611  fzo1fzo0n0  13617  elfzodifsumelfzo  13633  elfznelfzo  13675  injresinj  13693  mulexp  14010  expadd  14013  expmul  14016  facdiv  14196  hashgt12el2  14332  hashimarni  14350  leisorel  14369  fi1uzind  14416  pfxfv  14592  swrdswrdlem  14613  pfxccat3  14643  reuccatpfxs1lem  14655  repswswrd  14693  cshf1  14719  2cshwcshw  14734  cshimadifsn  14738  relexpindlem  14972  pwdif  15777  dvdsaddre2b  16220  addmodlteqALT  16238  ltoddhalfle  16274  halfleoddlt  16275  coprmprod  16574  coprmproddvds  16576  cncongr1  16580  oddprmgt2  16612  prmfac1  16633  infpnlem1  16824  prmgaplem5  16969  prmgaplem6  16970  cshwshashlem1  17009  setsstruct  17089  iscatd2  17589  initoeu2lem2  17924  clatleglb  18426  dfgrp3e  18955  mulgaddcom  19013  mulginvcom  19014  symgfvne  19295  lsmcv  21080  assamulgscm  21840  psrvscafval  21887  mat1scmat  22455  cramer0  22606  chpscmat  22758  fvmptnn04ifa  22766  fvmptnn04ifc  22768  fvmptnn04ifd  22769  fiinopn  22817  opnneissb  23030  cnpimaex  23172  regsep  23250  hausnei2  23269  cmpsublem  23315  cmpsub  23316  filufint  23836  blssps  24340  blss  24341  mblsplit  25461  dvply2g  26220  taylply2  26303  bcmono  27216  gausslemma2dlem1a  27304  2sqlem10  27367  eqscut3  27766  addsuniflem  27945  negsunif  27998  ssltmul2  28088  precsexlem11  28156  elntg2  28965  upgrex  29072  numedglnl  29124  ausgrumgri  29147  ausgrusgri  29148  usgredg2vtxeuALT  29202  ushgredgedg  29209  ushgredgedgloop  29211  edg0usgr  29233  0uhgrsubgr  29259  subumgredg2  29265  fusgrfisbase  29308  cusgrsizeinds  29433  cusgrsize2inds  29434  finsumvtxdg2size  29531  upgrewlkle2  29587  wlkl1loop  29618  pthdivtx  29707  2pthnloop  29711  upgrwlkdvde  29717  uhgrwkspthlem2  29734  usgr2pthlem  29743  usgr2pth  29744  clwlkl1loop  29763  crctcshwlkn0lem4  29793  wwlksnextproplem3  29891  wspn0  29904  umgr2adedgwlkonALT  29927  umgr2wlk  29929  umgr2wlkon  29930  elwwlks2  29949  clwwlkccatlem  29971  umgrclwwlkge2  29973  clwlkclwwlklem2  29982  clwlkclwwlkf1lem2  29987  clwlkclwwlkf  29990  clwwlknlbonbgr1  30021  clwwlkn1loopb  30025  clwwlkel  30028  clwwlkext2edg  30038  clwwlknonex2lem2  30090  clwwlknonex2  30091  clwwlknonex2e  30092  1pthon2v  30135  uhgr3cyclex  30164  eupth2lem3lem6  30215  frgr3vlem1  30255  3cyclfrgrrn1  30267  frgrnbnb  30275  frgrwopreglem4a  30292  2clwwlk2clwwlklem  30328  wlkl0  30349  frgrregord013  30377  frgrregord13  30378  frgrogt3nreg  30379  friendship  30381  chcompl  31224  spansncol  31550  hoaddsub  31798  bnj600  34952  sconnpht  35294  satffunlem  35466  satfvel  35477  msubvrs  35625  funpsstri  35831  imp5p  36376  cntotbnd  37856  clmgmOLD  37911  grpomndo  37935  rngoneglmul  38003  rngonegrmul  38004  zerdivemp1x  38007  atlex  39435  cvlexch1  39447  cvlsupr4  39464  cvlsupr5  39465  cvlsupr6  39466  2llnneN  39528  athgt  39575  llnle  39637  lplnle  39659  lvoli2  39700  pmaple  39880  dalawlem10  39999  dalawlem13  40002  dalawlem14  40003  dalaw  40005  lhp2lt  40120  ldilval  40232  cdleme50trn2  40670  cdlemf  40682  cdlemg18b  40798  tendotp  40880  tendospcanN  41142  dihmeetlem3N  41424  dvh4dimlem  41562  pell14qrexpclnn0  42983  pell1qrgap  42991  aomclem2  43172  rngunsnply  43286  dflim5  43446  relexpaddss  43835  rp-simp2  43910  gneispaceel2  44261  bi33imp12  44608  bi13imp23  44609  bi23imp1  44612  bi123imp0  44613  ee333  44624  jaoded  44683  e333  44849  suctrALTcf  45038  suctrALTcfVD  45039  ax6e2ndeqALT  45047  mullimc  45740  mullimcf  45747  f1oresf1o2  47415  fzopredsuc  47447  subsubelfzo0  47450  2tceilhalfelfzo1  47456  elsetpreimafvbi  47515  iccpartimp  47541  iccpartigtl  47547  lswn0  47568  poprelb  47648  fmtnofac1  47694  lighneallem2  47730  lighneallem3  47731  lighneallem4  47734  mogoldbblem  47844  fpprel2  47865  gbegt5  47885  sbgoldbaltlem1  47903  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  clnbgrssedg  47965  grimuhgr  48011  uhgrimedgi  48014  uhgrimisgrgriclem  48054  uhgrimisgrgric  48055  clnbgrgrim  48058  grimedg  48059  grimgrtri  48073  usgrgrtrirex  48074  isubgr3stgrlem4  48093  grlimgrtri  48127  clnbgr3stgrgrlim  48143  gpgedgvtx1  48186  gpgvtxedg0  48187  gpgvtxedg1  48188  gpgcubic  48203  gpg5nbgr3star  48205  lidldomn1  48355  cznnring  48386  rngccatidALTV  48396  ringccatidALTV  48430  scmsuppss  48495  lmodvsmdi  48503  gsumlsscl  48504  lindslinindimp2lem1  48583  lindsrng01  48593  elfzolborelfzop1  48644  fllog2  48693  dignn0flhalflem1  48740  rrxlinesc  48860  itschlc0yqe  48885  itsclc0xyqsol  48893  itscnhlinecirc02p  48910