Theorem 3imp 1108

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3imp31  1109  3imp231  1110  3impb  1112  3impib  1113  3imp1  1344  3impd  1345  3jao  1422  biimp3ar  1467  3elpr2eq  4912  wefrc  5676  iotan0  6544  f1ssf1  6875  fveqdmss  7092  funelss  8061  poxp  8142  fvn0elsuppb  8195  suppfnss  8203  smo11  8394  odi  8609  omass  8610  nndi  8653  nnmass  8654  undifixp  8963  domunfican  9363  preleqg  9658  pr2nelemOLD  10046  dfac8alem  10072  fin33i  10412  domtriomlem  10485  axdc3lem2  10494  axdc3lem4  10496  axdc4lem  10498  ttukeyg  10560  axdclem  10562  grupr  10840  nqereu  10972  squeeze0  12169  rpnnen1lem5  13017  xnn0lenn0nn0  13278  supxrun  13349  difelfzle  13668  elfzo0z  13728  fzofzim  13733  fzo1fzo0n0  13737  elfzodifsumelfzo  13752  elfznelfzo  13792  injresinj  13808  mulexp  14121  expadd  14124  expmul  14127  facdiv  14304  hashgt12el2  14440  hashimarni  14458  leisorel  14479  fi1uzind  14516  pfxfv  14690  swrdswrdlem  14712  pfxccat3  14742  reuccatpfxs1lem  14754  repswswrd  14792  cshf1  14818  2cshwcshw  14834  cshimadifsn  14838  relexpindlem  15068  pwdif  15872  dvdsaddre2b  16309  addmodlteqALT  16327  ltoddhalfle  16363  halfleoddlt  16364  coprmprod  16662  coprmproddvds  16664  cncongr1  16668  oddprmgt2  16700  prmfac1  16722  infpnlem1  16912  prmgaplem5  17057  prmgaplem6  17058  cshwshashlem1  17098  setsstruct  17178  iscatd2  17694  initoeu2lem2  18037  clatleglb  18543  dfgrp3e  19034  mulgaddcom  19092  mulginvcom  19093  symgfvne  19378  lsmcv  21122  assamulgscm  21898  psrvscafval  21957  mat1scmat  22532  cramer0  22683  chpscmat  22835  fvmptnn04ifa  22843  fvmptnn04ifc  22845  fvmptnn04ifd  22846  fiinopn  22894  opnneissb  23109  cnpimaex  23251  regsep  23329  hausnei2  23348  cmpsublem  23394  cmpsub  23395  filufint  23915  blssps  24421  blss  24422  mblsplit  25552  dvply2g  26312  taylply2  26395  bcmono  27306  gausslemma2dlem1a  27394  2sqlem10  27457  addsuniflem  28015  negsunif  28064  ssltmul2  28149  precsexlem11  28216  elntg2  28919  upgrex  29028  numedglnl  29080  ausgrumgri  29103  ausgrusgri  29104  usgredg2vtxeuALT  29158  ushgredgedg  29165  ushgredgedgloop  29167  edg0usgr  29189  0uhgrsubgr  29215  subumgredg2  29221  fusgrfisbase  29264  cusgrsizeinds  29389  cusgrsize2inds  29390  finsumvtxdg2size  29487  upgrewlkle2  29543  wlkl1loop  29575  pthdivtx  29666  2pthnloop  29668  upgrwlkdvde  29674  uhgrwkspthlem2  29691  usgr2pthlem  29700  usgr2pth  29701  clwlkl1loop  29720  crctcshwlkn0lem4  29747  wwlksnextproplem3  29845  wspn0  29858  umgr2adedgwlkonALT  29881  umgr2wlk  29883  umgr2wlkon  29884  elwwlks2  29900  clwwlkccatlem  29922  umgrclwwlkge2  29924  clwlkclwwlklem2  29933  clwlkclwwlkf1lem2  29938  clwlkclwwlkf  29941  clwwlknlbonbgr1  29972  clwwlkn1loopb  29976  clwwlkel  29979  clwwlkext2edg  29989  clwwlknonex2lem2  30041  clwwlknonex2  30042  clwwlknonex2e  30043  1pthon2v  30086  uhgr3cyclex  30115  eupth2lem3lem6  30166  frgr3vlem1  30206  3cyclfrgrrn1  30218  frgrnbnb  30226  frgrwopreglem4a  30243  2clwwlk2clwwlklem  30279  wlkl0  30300  frgrregord013  30328  frgrregord13  30329  frgrogt3nreg  30330  friendship  30332  chcompl  31175  spansncol  31501  hoaddsub  31749  bnj600  34764  sconnpht  35057  satffunlem  35229  satfvel  35240  msubvrs  35388  funpsstri  35589  imp5p  36023  cntotbnd  37497  clmgmOLD  37552  grpomndo  37576  rngoneglmul  37644  rngonegrmul  37645  zerdivemp1x  37648  atlex  39014  cvlexch1  39026  cvlsupr4  39043  cvlsupr5  39044  cvlsupr6  39045  2llnneN  39108  athgt  39155  llnle  39217  lplnle  39239  lvoli2  39280  pmaple  39460  dalawlem10  39579  dalawlem13  39582  dalawlem14  39583  dalaw  39585  lhp2lt  39700  ldilval  39812  cdleme50trn2  40250  cdlemf  40262  cdlemg18b  40378  tendotp  40460  tendospcanN  40722  dihmeetlem3N  41004  dvh4dimlem  41142  pell14qrexpclnn0  42523  pell1qrgap  42531  aomclem2  42716  rngunsnply  42834  dflim5  42995  relexpaddss  43385  rp-simp2  43460  gneispaceel2  43811  bi33imp12  44166  bi23imp13  44167  bi13imp23  44168  bi23imp1  44171  bi123imp0  44172  ee333  44183  jaoded  44242  e333  44409  suctrALTcf  44598  suctrALTcfVD  44599  ax6e2ndeqALT  44607  mullimc  45237  mullimcf  45244  f1oresf1o2  46904  fzopredsuc  46936  subsubelfzo0  46939  elsetpreimafvbi  46963  iccpartimp  46989  iccpartigtl  46995  lswn0  47016  poprelb  47096  fmtnofac1  47142  lighneallem2  47178  lighneallem3  47179  lighneallem4  47182  mogoldbblem  47292  fpprel2  47313  gbegt5  47333  sbgoldbaltlem1  47351  bgoldbtbndlem2  47378  bgoldbtbndlem3  47379  grimuhgr  47457  uhgrimisgrgriclem  47477  uhgrimisgrgric  47478  clnbgrgrim  47481  lidldomn1  47608  cznnring  47639  rngccatidALTV  47649  ringccatidALTV  47683  scmsuppss  47751  lmodvsmdi  47761  gsumlsscl  47762  lindslinindimp2lem1  47841  lindsrng01  47851  elfzolborelfzop1  47902  difmodm1lt  47910  fllog2  47956  dignn0flhalflem1  48003  rrxlinesc  48123  itschlc0yqe  48148  itsclc0xyqsol  48156  itscnhlinecirc02p  48173