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 418	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3imp31  1111  3imp231  1112  3impb  1114  3impib  1115  3imp1  1346  3impd  1347  3jao  1424  biimp3ar  1469  3elpr2eq  4839  wefrc  5584  iotan0  6427  f1ssf1  6757  fveqdmss  6965  funelss  7897  poxp  7978  fvn0elsuppb  8006  suppfnss  8014  smo11  8204  odi  8419  omass  8420  nndi  8463  nnmass  8464  undifixp  8731  domunfican  9096  preleqg  9382  pr2nelem  9769  dfac8alem  9794  fin33i  10134  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  ttukeyg  10282  axdclem  10284  grupr  10562  nqereu  10694  squeeze0  11887  rpnnen1lem5  12730  xnn0lenn0nn0  12988  supxrun  13059  difelfzle  13378  elfzo0z  13438  fzofzim  13443  fzo1fzo0n0  13447  elfzodifsumelfzo  13462  elfznelfzo  13501  injresinj  13517  mulexp  13831  expadd  13834  expmul  13837  facdiv  14010  hashgt12el2  14147  hashimarni  14165  leisorel  14183  fi1uzind  14220  pfxfv  14404  swrdswrdlem  14426  pfxccat3  14456  reuccatpfxs1lem  14468  repswswrd  14506  cshf1  14532  2cshwcshw  14547  cshimadifsn  14551  relexpindlem  14783  pwdif  15589  dvdsaddre2b  16025  addmodlteqALT  16043  ltoddhalfle  16079  halfleoddlt  16080  coprmprod  16375  coprmproddvds  16377  cncongr1  16381  oddprmgt2  16413  prmfac1  16435  infpnlem1  16620  prmgaplem5  16765  prmgaplem6  16766  cshwshashlem1  16806  setsstruct  16886  iscatd2  17399  initoeu2lem2  17739  clatleglb  18245  dfgrp3e  18684  mulgaddcom  18736  mulginvcom  18737  symgfvne  18997  f1rhm0to0ALT  19994  lsmcv  20412  assamulgscm  21114  psrvscafval  21168  mat1scmat  21697  cramer0  21848  chpscmat  22000  fvmptnn04ifa  22008  fvmptnn04ifc  22010  fvmptnn04ifd  22011  fiinopn  22059  opnneissb  22274  cnpimaex  22416  regsep  22494  hausnei2  22513  cmpsublem  22559  cmpsub  22560  filufint  23080  blssps  23586  blss  23587  mblsplit  24705  bcmono  26434  gausslemma2dlem1a  26522  2sqlem10  26585  elntg2  27362  upgrex  27471  numedglnl  27523  ausgrumgri  27546  ausgrusgri  27547  usgredg2vtxeuALT  27598  ushgredgedg  27605  ushgredgedgloop  27607  edg0usgr  27629  0uhgrsubgr  27655  subumgredg2  27661  fusgrfisbase  27704  cusgrsizeinds  27828  cusgrsize2inds  27829  finsumvtxdg2size  27926  upgrewlkle2  27982  wlkl1loop  28014  pthdivtx  28106  2pthnloop  28108  upgrwlkdvde  28114  uhgrwkspthlem2  28131  usgr2pthlem  28140  usgr2pth  28141  clwlkl1loop  28160  crctcshwlkn0lem4  28187  wwlksnextproplem3  28285  wspn0  28298  umgr2adedgwlkonALT  28321  umgr2wlk  28323  umgr2wlkon  28324  elwwlks2  28340  clwwlkccatlem  28362  umgrclwwlkge2  28364  clwlkclwwlklem2  28373  clwlkclwwlkf1lem2  28378  clwlkclwwlkf  28381  clwwlknlbonbgr1  28412  clwwlkn1loopb  28416  clwwlkel  28419  clwwlkext2edg  28429  clwwlknonex2lem2  28481  clwwlknonex2  28482  clwwlknonex2e  28483  1pthon2v  28526  uhgr3cyclex  28555  eupth2lem3lem6  28606  frgr3vlem1  28646  3cyclfrgrrn1  28658  frgrnbnb  28666  frgrwopreglem4a  28683  2clwwlk2clwwlklem  28719  wlkl0  28740  frgrregord013  28768  frgrregord13  28769  frgrogt3nreg  28770  friendship  28772  chcompl  29613  spansncol  29939  hoaddsub  30187  bnj600  32908  sconnpht  33200  satffunlem  33372  satfvel  33383  msubvrs  33531  funpsstri  33748  imp5p  34509  cntotbnd  35963  clmgmOLD  36018  grpomndo  36042  rngoneglmul  36110  rngonegrmul  36111  zerdivemp1x  36114  atlex  37337  cvlexch1  37349  cvlsupr4  37366  cvlsupr5  37367  cvlsupr6  37368  2llnneN  37430  athgt  37477  llnle  37539  lplnle  37561  lvoli2  37602  pmaple  37782  dalawlem10  37901  dalawlem13  37904  dalawlem14  37905  dalaw  37907  lhp2lt  38022  ldilval  38134  cdleme50trn2  38572  cdlemf  38584  cdlemg18b  38700  tendotp  38782  tendospcanN  39044  dihmeetlem3N  39326  dvh4dimlem  39464  pell14qrexpclnn0  40695  pell1qrgap  40703  aomclem2  40887  rngunsnply  41005  relexpaddss  41333  rp-simp2  41408  gneispaceel2  41761  bi33imp12  42117  bi23imp13  42118  bi13imp23  42119  bi23imp1  42122  bi123imp0  42123  ee333  42134  jaoded  42193  e333  42360  suctrALTcf  42549  suctrALTcfVD  42550  ax6e2ndeqALT  42558  mullimc  43164  mullimcf  43171  f1oresf1o2  44794  fzopredsuc  44826  subsubelfzo0  44829  elsetpreimafvbi  44854  iccpartimp  44880  iccpartigtl  44886  lswn0  44907  poprelb  44987  fmtnofac1  45033  lighneallem2  45069  lighneallem3  45070  lighneallem4  45073  mogoldbblem  45183  fpprel2  45204  gbegt5  45224  sbgoldbaltlem1  45242  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  lidldomn1  45490  cznnring  45525  rngccatidALTV  45558  ringccatidALTV  45621  scmsuppss  45719  lmodvsmdi  45729  gsumlsscl  45730  lindslinindimp2lem1  45810  lindsrng01  45820  elfzolborelfzop1  45871  difmodm1lt  45879  fllog2  45925  dignn0flhalflem1  45972  rrxlinesc  46092  itschlc0yqe  46117  itsclc0xyqsol  46125  itscnhlinecirc02p  46142