Theorem 3imp 1112

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3imp31  1113  3imp231  1114  3impb  1116  3impib  1117  3imp1  1348  3impd  1349  3jao  1426  biimp3ar  1471  3elpr2eq  4908  wefrc  5671  iotan0  6534  f1ssf1  6866  fveqdmss  7081  funelss  8033  poxp  8114  fvn0elsuppb  8166  suppfnss  8174  smo11  8364  odi  8579  omass  8580  nndi  8623  nnmass  8624  undifixp  8928  domunfican  9320  preleqg  9610  pr2nelemOLD  9998  dfac8alem  10024  fin33i  10364  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  ttukeyg  10512  axdclem  10514  grupr  10792  nqereu  10924  squeeze0  12117  rpnnen1lem5  12965  xnn0lenn0nn0  13224  supxrun  13295  difelfzle  13614  elfzo0z  13674  fzofzim  13679  fzo1fzo0n0  13683  elfzodifsumelfzo  13698  elfznelfzo  13737  injresinj  13753  mulexp  14067  expadd  14070  expmul  14073  facdiv  14247  hashgt12el2  14383  hashimarni  14401  leisorel  14421  fi1uzind  14458  pfxfv  14632  swrdswrdlem  14654  pfxccat3  14684  reuccatpfxs1lem  14696  repswswrd  14734  cshf1  14760  2cshwcshw  14776  cshimadifsn  14780  relexpindlem  15010  pwdif  15814  dvdsaddre2b  16250  addmodlteqALT  16268  ltoddhalfle  16304  halfleoddlt  16305  coprmprod  16598  coprmproddvds  16600  cncongr1  16604  oddprmgt2  16636  prmfac1  16658  infpnlem1  16843  prmgaplem5  16988  prmgaplem6  16989  cshwshashlem1  17029  setsstruct  17109  iscatd2  17625  initoeu2lem2  17965  clatleglb  18471  dfgrp3e  18923  mulgaddcom  18978  mulginvcom  18979  symgfvne  19248  f1rhm0to0ALT  20280  lsmcv  20754  assamulgscm  21455  psrvscafval  21509  mat1scmat  22041  cramer0  22192  chpscmat  22344  fvmptnn04ifa  22352  fvmptnn04ifc  22354  fvmptnn04ifd  22355  fiinopn  22403  opnneissb  22618  cnpimaex  22760  regsep  22838  hausnei2  22857  cmpsublem  22903  cmpsub  22904  filufint  23424  blssps  23930  blss  23931  mblsplit  25049  bcmono  26780  gausslemma2dlem1a  26868  2sqlem10  26931  addsuniflem  27484  negsunif  27529  ssltmul2  27603  precsexlem11  27663  elntg2  28243  upgrex  28352  numedglnl  28404  ausgrumgri  28427  ausgrusgri  28428  usgredg2vtxeuALT  28479  ushgredgedg  28486  ushgredgedgloop  28488  edg0usgr  28510  0uhgrsubgr  28536  subumgredg2  28542  fusgrfisbase  28585  cusgrsizeinds  28709  cusgrsize2inds  28710  finsumvtxdg2size  28807  upgrewlkle2  28863  wlkl1loop  28895  pthdivtx  28986  2pthnloop  28988  upgrwlkdvde  28994  uhgrwkspthlem2  29011  usgr2pthlem  29020  usgr2pth  29021  clwlkl1loop  29040  crctcshwlkn0lem4  29067  wwlksnextproplem3  29165  wspn0  29178  umgr2adedgwlkonALT  29201  umgr2wlk  29203  umgr2wlkon  29204  elwwlks2  29220  clwwlkccatlem  29242  umgrclwwlkge2  29244  clwlkclwwlklem2  29253  clwlkclwwlkf1lem2  29258  clwlkclwwlkf  29261  clwwlknlbonbgr1  29292  clwwlkn1loopb  29296  clwwlkel  29299  clwwlkext2edg  29309  clwwlknonex2lem2  29361  clwwlknonex2  29362  clwwlknonex2e  29363  1pthon2v  29406  uhgr3cyclex  29435  eupth2lem3lem6  29486  frgr3vlem1  29526  3cyclfrgrrn1  29538  frgrnbnb  29546  frgrwopreglem4a  29563  2clwwlk2clwwlklem  29599  wlkl0  29620  frgrregord013  29648  frgrregord13  29649  frgrogt3nreg  29650  friendship  29652  chcompl  30495  spansncol  30821  hoaddsub  31069  bnj600  33930  sconnpht  34220  satffunlem  34392  satfvel  34403  msubvrs  34551  funpsstri  34737  imp5p  35196  cntotbnd  36664  clmgmOLD  36719  grpomndo  36743  rngoneglmul  36811  rngonegrmul  36812  zerdivemp1x  36815  atlex  38186  cvlexch1  38198  cvlsupr4  38215  cvlsupr5  38216  cvlsupr6  38217  2llnneN  38280  athgt  38327  llnle  38389  lplnle  38411  lvoli2  38452  pmaple  38632  dalawlem10  38751  dalawlem13  38754  dalawlem14  38755  dalaw  38757  lhp2lt  38872  ldilval  38984  cdleme50trn2  39422  cdlemf  39434  cdlemg18b  39550  tendotp  39632  tendospcanN  39894  dihmeetlem3N  40176  dvh4dimlem  40314  pell14qrexpclnn0  41604  pell1qrgap  41612  aomclem2  41797  rngunsnply  41915  dflim5  42079  relexpaddss  42469  rp-simp2  42544  gneispaceel2  42895  bi33imp12  43251  bi23imp13  43252  bi13imp23  43253  bi23imp1  43256  bi123imp0  43257  ee333  43268  jaoded  43327  e333  43494  suctrALTcf  43683  suctrALTcfVD  43684  ax6e2ndeqALT  43692  mullimc  44332  mullimcf  44339  f1oresf1o2  45999  fzopredsuc  46031  subsubelfzo0  46034  elsetpreimafvbi  46059  iccpartimp  46085  iccpartigtl  46091  lswn0  46112  poprelb  46192  fmtnofac1  46238  lighneallem2  46274  lighneallem3  46275  lighneallem4  46278  mogoldbblem  46388  fpprel2  46409  gbegt5  46429  sbgoldbaltlem1  46447  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  lidldomn1  46823  cznnring  46854  rngccatidALTV  46887  ringccatidALTV  46950  scmsuppss  47048  lmodvsmdi  47058  gsumlsscl  47059  lindslinindimp2lem1  47139  lindsrng01  47149  elfzolborelfzop1  47200  difmodm1lt  47208  fllog2  47254  dignn0flhalflem1  47301  rrxlinesc  47421  itschlc0yqe  47446  itsclc0xyqsol  47454  itscnhlinecirc02p  47471