Theorem 3imp 1130

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  3imp31  1132  3imp231  1133  3impaOLD  1135  3impb  1136  3impib  1137  3impiaOLD  1139  syl3an2OLD  1197  syl3an3OLD  1199  3com23OLD  1442  3imp21OLD  1444  3an1rsOLD  1447  3imp1  1449  3impd  1450  3jao  1542  3jaoOLD  1543  biimp3ar  1587  3elpr2eq  4629  wefrc  5305  predpo  5911  f1ssf1  6384  fveqdmss  6576  poxp  7523  fvn0elsuppb  7546  suppfnss  7554  smo11  7697  odi  7896  omass  7897  nndi  7940  nnmass  7941  undifixp  8181  isinf  8412  domunfican  8472  infssuni  8496  preleqg  8757  pr2nelem  9110  dfac8alem  9135  fin33i  9476  fin1a2lem10  9516  domtriomlem  9549  axdc3lem2  9558  axdc3lem4  9560  axdc4lem  9562  ttukeyg  9624  axdclem  9626  grupr  9904  nqereu  10036  squeeze0  11211  rpnnen1lem5  12037  xnn0lenn0nn0  12293  supxrun  12364  difelfzle  12676  elfzo0z  12734  fzofzim  12739  fzo1fzo0n0  12743  elfzodifsumelfzo  12758  elfznelfzo  12797  injresinj  12813  mulexp  13122  expadd  13125  expmul  13128  bernneq  13213  facdiv  13294  hashgt12el2  13428  hashimarni  13445  leisorel  13461  fi1uzind  13496  2swrd1eqwrdeq  13678  swrdswrdlem  13683  swrdccat3  13716  swrdccatid  13721  repswswrd  13755  cshf1  13780  2cshwcshw  13795  cshimadifsn  13799  swrdco  13807  relexpindlem  14026  dvdsaddre2b  15252  addmodlteqALT  15270  ltoddhalfle  15305  halfleoddlt  15306  dfgcd2  15482  coprmprod  15593  coprmproddvds  15595  cncongr1  15599  oddprmgt2  15629  prmfac1  15648  infpnlem1  15831  prmgaplem5  15976  prmgaplem6  15977  cshwshashlem1  16014  setsstruct  16109  iscatd2  16546  initoeu2lem2  16869  clatleglb  17331  dfgrp3e  17720  mulgaddcom  17768  mulginvcom  17769  symgfvne  18009  f1rhm0to0ALT  18945  lmodvsmmulgdi  19102  lsmcv  19349  assamulgscm  19559  psrvscafval  19599  mamufacex  20405  mat1scmat  20556  gsummatr01lem4  20676  cramer0  20709  chpscmat  20860  fvmptnn04ifa  20868  fvmptnn04ifc  20870  fvmptnn04ifd  20871  fiinopn  20919  opnneissb  21132  cnpimaex  21274  regsep  21352  hausnei2  21371  cmpsublem  21416  cmpsub  21417  filufint  21937  blssps  22442  blss  22443  mblsplit  23513  bcmono  25216  gausslemma2dlem1a  25304  2sqlem10  25367  upgrex  26201  numedglnl  26254  ausgrumgri  26277  ausgrusgri  26278  usgredg2vtxeuALT  26329  ushgredgedg  26336  ushgredgedgloop  26338  ushgredgedgloopOLD  26339  edg0usgr  26361  0uhgrsubgr  26387  subumgredg2  26393  fusgrfisbase  26436  cusgrsizeinds  26576  cusgrsize2inds  26577  finsumvtxdg2size  26674  upgrewlkle2  26730  wlkl1loop  26762  pthdivtx  26853  2pthnloop  26855  upgrwlkdvde  26861  uhgrwkspthlem2  26878  usgr2pthlem  26887  usgr2pth  26888  clwlkl1loop  26907  crctcshwlkn0lem4  26934  wwlksnextproplem3  27049  wspn0  27064  umgr2adedgwlkonALT  27087  umgr2wlk  27089  umgr2wlkon  27090  elwwlks2  27108  clwwlkccatlem  27132  umgrclwwlkge2  27134  clwlkclwwlklem2  27143  clwlkclwwlkf1lem2  27148  clwlkclwwlkf  27151  clwwlknlbonbgr1  27188  clwwlkn1loopb  27192  clwwlkel  27195  clwwlkext2edg  27206  clwwlknonex2lem2  27277  clwwlknonex2  27278  clwwlknonex2e  27279  1pthon2v  27326  uhgr3cyclex  27355  eupth2lem3lem6  27406  frgr3vlem1  27448  3cyclfrgrrn1  27460  frgrnbnb  27468  frgrwopreglem4a  27485  2clwwlk2clwwlklem  27523  wlkl0  27547  frgrregord013  27583  frgrregord13  27584  frgrogt3nreg  27585  friendship  27587  chcompl  28427  spansncol  28755  hoaddsub  29003  bnj600  31312  sconnpht  31534  msubvrs  31780  funpsstri  31985  imp5p  32626  cntotbnd  33906  clmgmOLD  33961  grpomndo  33985  rngoneglmul  34053  rngonegrmul  34054  zerdivemp1x  34057  atlex  35096  cvlexch1  35108  cvlsupr4  35125  cvlsupr5  35126  cvlsupr6  35127  2llnneN  35189  athgt  35236  llnle  35298  lplnle  35320  lvoli2  35361  pmaple  35541  dalawlem10  35660  dalawlem13  35663  dalawlem14  35664  dalaw  35666  lhp2lt  35781  ldilval  35893  cdleme50trn2  36332  cdlemf  36344  cdlemg18b  36460  tendotp  36542  tendospcanN  36804  dihmeetlem3N  37086  dvh4dimlem  37224  pell14qrexpclnn0  37932  pell1qrgap  37940  aomclem2  38126  rngunsnply  38244  relexpxpmin  38509  relexpaddss  38510  rp-simp2  38587  gneispaceel2  38942  bi33imp12  39194  bi23imp13  39195  bi13imp23  39196  bi23imp1  39199  bi123imp0  39200  ee333  39211  jaoded  39280  e333  39457  suctrALTcf  39652  suctrALTcfVD  39653  ax6e2ndeqALT  39661  mullimc  40328  mullimcf  40335  f1oresf1o2  41881  fzopredsuc  41908  subsubelfzo0  41911  iccpartimp  41928  iccpartigtl  41934  lswn0  41955  pfxfv  41974  pfxccat3  42001  reuccatpfxs1lem  42008  fmtnofac1  42057  pwdif  42076  lighneallem2  42098  lighneallem3  42099  lighneallem4  42102  mogoldbblem  42204  gbegt5  42224  sbgoldbaltlem1  42242  bgoldbtbndlem2  42269  bgoldbtbndlem3  42270  lidldomn1  42489  cznnring  42524  rngccatidALTV  42557  ringccatidALTV  42620  scmsuppss  42721  lmodvsmdi  42731  gsumlsscl  42732  lindslinindimp2lem1  42815  lindsrng01  42825  elfzolborelfzop1  42877  difmodm1lt  42885  fllog2  42930  dignn0flhalflem1  42977