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  4847  wefrc  5599  iotan0  6453  f1ssf1  6783  fveqdmss  6993  funelss  7931  poxp  8011  fvn0elsuppb  8042  suppfnss  8050  smo11  8240  odi  8456  omass  8457  nndi  8500  nnmass  8501  undifixp  8768  domunfican  9155  preleqg  9441  pr2nelemOLD  9829  dfac8alem  9855  fin33i  10195  domtriomlem  10268  axdc3lem2  10277  axdc3lem4  10279  axdc4lem  10281  ttukeyg  10343  axdclem  10345  grupr  10623  nqereu  10755  squeeze0  11948  rpnnen1lem5  12791  xnn0lenn0nn0  13049  supxrun  13120  difelfzle  13439  elfzo0z  13499  fzofzim  13504  fzo1fzo0n0  13508  elfzodifsumelfzo  13523  elfznelfzo  13562  injresinj  13578  mulexp  13892  expadd  13895  expmul  13898  facdiv  14071  hashgt12el2  14207  hashimarni  14225  leisorel  14243  fi1uzind  14280  pfxfv  14464  swrdswrdlem  14486  pfxccat3  14516  reuccatpfxs1lem  14528  repswswrd  14566  cshf1  14592  2cshwcshw  14607  cshimadifsn  14611  relexpindlem  14843  pwdif  15649  dvdsaddre2b  16085  addmodlteqALT  16103  ltoddhalfle  16139  halfleoddlt  16140  coprmprod  16433  coprmproddvds  16435  cncongr1  16439  oddprmgt2  16471  prmfac1  16493  infpnlem1  16678  prmgaplem5  16823  prmgaplem6  16824  cshwshashlem1  16864  setsstruct  16944  iscatd2  17457  initoeu2lem2  17797  clatleglb  18303  dfgrp3e  18742  mulgaddcom  18794  mulginvcom  18795  symgfvne  19055  f1rhm0to0ALT  20052  lsmcv  20474  assamulgscm  21176  psrvscafval  21230  mat1scmat  21759  cramer0  21910  chpscmat  22062  fvmptnn04ifa  22070  fvmptnn04ifc  22072  fvmptnn04ifd  22073  fiinopn  22121  opnneissb  22336  cnpimaex  22478  regsep  22556  hausnei2  22575  cmpsublem  22621  cmpsub  22622  filufint  23142  blssps  23648  blss  23649  mblsplit  24767  bcmono  26496  gausslemma2dlem1a  26584  2sqlem10  26647  elntg2  27461  upgrex  27570  numedglnl  27622  ausgrumgri  27645  ausgrusgri  27646  usgredg2vtxeuALT  27697  ushgredgedg  27704  ushgredgedgloop  27706  edg0usgr  27728  0uhgrsubgr  27754  subumgredg2  27760  fusgrfisbase  27803  cusgrsizeinds  27927  cusgrsize2inds  27928  finsumvtxdg2size  28025  upgrewlkle2  28081  wlkl1loop  28113  pthdivtx  28205  2pthnloop  28207  upgrwlkdvde  28213  uhgrwkspthlem2  28230  usgr2pthlem  28239  usgr2pth  28240  clwlkl1loop  28259  crctcshwlkn0lem4  28286  wwlksnextproplem3  28384  wspn0  28397  umgr2adedgwlkonALT  28420  umgr2wlk  28422  umgr2wlkon  28423  elwwlks2  28439  clwwlkccatlem  28461  umgrclwwlkge2  28463  clwlkclwwlklem2  28472  clwlkclwwlkf1lem2  28477  clwlkclwwlkf  28480  clwwlknlbonbgr1  28511  clwwlkn1loopb  28515  clwwlkel  28518  clwwlkext2edg  28528  clwwlknonex2lem2  28580  clwwlknonex2  28581  clwwlknonex2e  28582  1pthon2v  28625  uhgr3cyclex  28654  eupth2lem3lem6  28705  frgr3vlem1  28745  3cyclfrgrrn1  28757  frgrnbnb  28765  frgrwopreglem4a  28782  2clwwlk2clwwlklem  28818  wlkl0  28839  frgrregord013  28867  frgrregord13  28868  frgrogt3nreg  28869  friendship  28871  chcompl  29712  spansncol  30038  hoaddsub  30286  bnj600  33005  sconnpht  33297  satffunlem  33469  satfvel  33480  msubvrs  33628  funpsstri  33842  imp5p  34561  cntotbnd  36014  clmgmOLD  36069  grpomndo  36093  rngoneglmul  36161  rngonegrmul  36162  zerdivemp1x  36165  atlex  37542  cvlexch1  37554  cvlsupr4  37571  cvlsupr5  37572  cvlsupr6  37573  2llnneN  37635  athgt  37682  llnle  37744  lplnle  37766  lvoli2  37807  pmaple  37987  dalawlem10  38106  dalawlem13  38109  dalawlem14  38110  dalaw  38112  lhp2lt  38227  ldilval  38339  cdleme50trn2  38777  cdlemf  38789  cdlemg18b  38905  tendotp  38987  tendospcanN  39249  dihmeetlem3N  39531  dvh4dimlem  39669  pell14qrexpclnn0  40898  pell1qrgap  40906  aomclem2  41091  rngunsnply  41209  relexpaddss  41554  rp-simp2  41629  gneispaceel2  41982  bi33imp12  42338  bi23imp13  42339  bi13imp23  42340  bi23imp1  42343  bi123imp0  42344  ee333  42355  jaoded  42414  e333  42581  suctrALTcf  42770  suctrALTcfVD  42771  ax6e2ndeqALT  42779  mullimc  43401  mullimcf  43408  f1oresf1o2  45042  fzopredsuc  45074  subsubelfzo0  45077  elsetpreimafvbi  45102  iccpartimp  45128  iccpartigtl  45134  lswn0  45155  poprelb  45235  fmtnofac1  45281  lighneallem2  45317  lighneallem3  45318  lighneallem4  45321  mogoldbblem  45431  fpprel2  45452  gbegt5  45472  sbgoldbaltlem1  45490  bgoldbtbndlem2  45517  bgoldbtbndlem3  45518  lidldomn1  45738  cznnring  45773  rngccatidALTV  45806  ringccatidALTV  45869  scmsuppss  45967  lmodvsmdi  45977  gsumlsscl  45978  lindslinindimp2lem1  46058  lindsrng01  46068  elfzolborelfzop1  46119  difmodm1lt  46127  fllog2  46173  dignn0flhalflem1  46220  rrxlinesc  46340  itschlc0yqe  46365  itsclc0xyqsol  46373  itscnhlinecirc02p  46390