Theorem 3imp 1111

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3imp31  1112  3imp231  1113  3impb  1115  bi23imp13  1116  3impib  1117  3imp1  1348  3impd  1349  3jao  1427  biimp3ar  1472  3elpr2eq  4906  wefrc  5679  iotan0  6551  f1ssf1  6880  fveqdmss  7098  funelss  8072  poxp  8153  fvn0elsuppb  8206  suppfnss  8214  smo11  8404  odi  8617  omass  8618  nndi  8661  nnmass  8662  undifixp  8974  domunfican  9361  preleqg  9655  pr2nelemOLD  10043  dfac8alem  10069  fin33i  10409  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  ttukeyg  10557  axdclem  10559  grupr  10837  nqereu  10969  squeeze0  12171  rpnnen1lem5  13023  xnn0lenn0nn0  13287  supxrun  13358  difelfzle  13681  elfzo0z  13741  fzofzim  13749  fzo1fzo0n0  13754  elfzodifsumelfzo  13770  elfznelfzo  13811  injresinj  13827  mulexp  14142  expadd  14145  expmul  14148  facdiv  14326  hashgt12el2  14462  hashimarni  14480  leisorel  14499  fi1uzind  14546  pfxfv  14720  swrdswrdlem  14742  pfxccat3  14772  reuccatpfxs1lem  14784  repswswrd  14822  cshf1  14848  2cshwcshw  14864  cshimadifsn  14868  relexpindlem  15102  pwdif  15904  dvdsaddre2b  16344  addmodlteqALT  16362  ltoddhalfle  16398  halfleoddlt  16399  coprmprod  16698  coprmproddvds  16700  cncongr1  16704  oddprmgt2  16736  prmfac1  16757  infpnlem1  16948  prmgaplem5  17093  prmgaplem6  17094  cshwshashlem1  17133  setsstruct  17213  iscatd2  17724  initoeu2lem2  18060  clatleglb  18563  dfgrp3e  19058  mulgaddcom  19116  mulginvcom  19117  symgfvne  19398  lsmcv  21143  assamulgscm  21921  psrvscafval  21968  mat1scmat  22545  cramer0  22696  chpscmat  22848  fvmptnn04ifa  22856  fvmptnn04ifc  22858  fvmptnn04ifd  22859  fiinopn  22907  opnneissb  23122  cnpimaex  23264  regsep  23342  hausnei2  23361  cmpsublem  23407  cmpsub  23408  filufint  23928  blssps  24434  blss  24435  mblsplit  25567  dvply2g  26326  taylply2  26409  bcmono  27321  gausslemma2dlem1a  27409  2sqlem10  27472  addsuniflem  28034  negsunif  28087  ssltmul2  28174  precsexlem11  28241  elntg2  29000  upgrex  29109  numedglnl  29161  ausgrumgri  29184  ausgrusgri  29185  usgredg2vtxeuALT  29239  ushgredgedg  29246  ushgredgedgloop  29248  edg0usgr  29270  0uhgrsubgr  29296  subumgredg2  29302  fusgrfisbase  29345  cusgrsizeinds  29470  cusgrsize2inds  29471  finsumvtxdg2size  29568  upgrewlkle2  29624  wlkl1loop  29656  pthdivtx  29747  2pthnloop  29751  upgrwlkdvde  29757  uhgrwkspthlem2  29774  usgr2pthlem  29783  usgr2pth  29784  clwlkl1loop  29803  crctcshwlkn0lem4  29833  wwlksnextproplem3  29931  wspn0  29944  umgr2adedgwlkonALT  29967  umgr2wlk  29969  umgr2wlkon  29970  elwwlks2  29986  clwwlkccatlem  30008  umgrclwwlkge2  30010  clwlkclwwlklem2  30019  clwlkclwwlkf1lem2  30024  clwlkclwwlkf  30027  clwwlknlbonbgr1  30058  clwwlkn1loopb  30062  clwwlkel  30065  clwwlkext2edg  30075  clwwlknonex2lem2  30127  clwwlknonex2  30128  clwwlknonex2e  30129  1pthon2v  30172  uhgr3cyclex  30201  eupth2lem3lem6  30252  frgr3vlem1  30292  3cyclfrgrrn1  30304  frgrnbnb  30312  frgrwopreglem4a  30329  2clwwlk2clwwlklem  30365  wlkl0  30386  frgrregord013  30414  frgrregord13  30415  frgrogt3nreg  30416  friendship  30418  chcompl  31261  spansncol  31587  hoaddsub  31835  bnj600  34933  sconnpht  35234  satffunlem  35406  satfvel  35417  msubvrs  35565  funpsstri  35766  imp5p  36312  cntotbnd  37803  clmgmOLD  37858  grpomndo  37882  rngoneglmul  37950  rngonegrmul  37951  zerdivemp1x  37954  atlex  39317  cvlexch1  39329  cvlsupr4  39346  cvlsupr5  39347  cvlsupr6  39348  2llnneN  39411  athgt  39458  llnle  39520  lplnle  39542  lvoli2  39583  pmaple  39763  dalawlem10  39882  dalawlem13  39885  dalawlem14  39886  dalaw  39888  lhp2lt  40003  ldilval  40115  cdleme50trn2  40553  cdlemf  40565  cdlemg18b  40681  tendotp  40763  tendospcanN  41025  dihmeetlem3N  41307  dvh4dimlem  41445  pell14qrexpclnn0  42877  pell1qrgap  42885  aomclem2  43067  rngunsnply  43181  dflim5  43342  relexpaddss  43731  rp-simp2  43806  gneispaceel2  44157  bi33imp12  44511  bi13imp23  44512  bi23imp1  44515  bi123imp0  44516  ee333  44527  jaoded  44586  e333  44753  suctrALTcf  44942  suctrALTcfVD  44943  ax6e2ndeqALT  44951  mullimc  45631  mullimcf  45638  f1oresf1o2  47303  fzopredsuc  47335  subsubelfzo0  47338  elsetpreimafvbi  47378  iccpartimp  47404  iccpartigtl  47410  lswn0  47431  poprelb  47511  fmtnofac1  47557  lighneallem2  47593  lighneallem3  47594  lighneallem4  47597  mogoldbblem  47707  fpprel2  47728  gbegt5  47748  sbgoldbaltlem1  47766  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  clnbgrssedg  47827  grimuhgr  47878  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrim  47902  grimedg  47903  grimgrtri  47916  usgrgrtrirex  47917  isubgr3stgrlem4  47936  grlimgrtri  47963  2tceilhalfelfzo1  48018  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpgcubic  48035  gpg5nbgr3star  48037  lidldomn1  48147  cznnring  48178  rngccatidALTV  48188  ringccatidALTV  48222  scmsuppss  48287  lmodvsmdi  48295  gsumlsscl  48296  lindslinindimp2lem1  48375  lindsrng01  48385  elfzolborelfzop1  48436  difmodm1lt  48443  fllog2  48489  dignn0flhalflem1  48536  rrxlinesc  48656  itschlc0yqe  48681  itsclc0xyqsol  48689  itscnhlinecirc02p  48706