Theorem 3imp 1126

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3imp31  1127  3imp231  1128  3impb  1130  bi23imp13  1131  3impib  1132  3imp1  1364  3impd  1365  3jao  1448  biimp3ar  1494  3elpr2eq  4867  wefrc  5646  iotan0  6515  f1ssf1  6843  fveqdmss  7063  funelss  8032  poxp  8112  fvn0elsuppb  8165  suppfnss  8173  smo11  8339  odi  8552  omass  8553  nndi  8597  nnmass  8598  undifixp  8920  domunfican  9269  preleqg  9572  dfac8alem  10001  fin33i  10341  domtriomlem  10414  axdc3lem2  10423  axdc3lem4  10425  axdc4lem  10427  ttukeyg  10489  axdclem  10491  grupr  10770  nqereu  10902  squeeze0  12109  rpnnen1lem5  12996  xnn0lenn0nn0  13262  supxrun  13333  difelfzle  13660  elfzo0z  13721  fzofzim  13729  fzo1fzo0n0  13735  elfzodifsumelfzo  13751  elfznelfzo  13793  injresinj  13811  mulexp  14128  expadd  14131  expmul  14134  facdiv  14314  hashgt12el2  14450  hashimarni  14468  leisorel  14487  fi1uzind  14534  pfxfv  14710  swrdswrdlem  14731  pfxccat3  14761  reuccatpfxs1lem  14773  repswswrd  14811  cshf1  14837  2cshwcshw  14852  cshimadifsn  14856  relexpindlem  15090  pwdif  15912  dvdsaddre2b  16355  addmodlteqALT  16373  ltoddhalfle  16409  halfleoddlt  16410  coprmprod  16709  coprmproddvds  16711  cncongr1  16715  oddprmgt2  16748  prmfac1  16769  infpnlem1  16960  prmgaplem5  17105  prmgaplem6  17106  cshwshashlem1  17145  setsstruct  17226  iscatd2  17727  initoeu2lem2  18062  clatleglb  18564  dfgrp3e  19097  mulgaddcom  19155  mulginvcom  19156  symgfvne  19442  lsmcv  21234  lidlunin0  21330  assamulgscm  22011  psrvscafval  22058  mat1scmat  22657  cramer0  22808  chpscmat  22960  fvmptnn04ifa  22968  fvmptnn04ifc  22970  fvmptnn04ifd  22971  fiinopn  23019  opnneissb  23232  cnpimaex  23374  regsep  23452  hausnei2  23471  cmpsublem  23517  cmpsub  23518  filufint  24038  blssps  24542  blss  24543  mblsplit  25652  dvply2g  26407  taylply2  26489  bcmono  27399  gausslemma2dlem1a  27487  2sqlem10  27550  eqcuts3  27955  addsuniflem  28152  negsunif  28206  sltmuls2  28299  precsexlem11  28368  bdaypw2n0bndlem  28614  elreno2  28646  elntg2  29244  upgrex  29351  numedglnl  29403  ausgrumgri  29426  ausgrusgri  29427  usgredg2vtxeuALT  29481  ushgredgedg  29488  ushgredgedgloop  29490  edg0usgr  29512  0uhgrsubgr  29538  subumgredg2  29544  fusgrfisbase  29587  cusgrsizeinds  29711  cusgrsize2inds  29712  finsumvtxdg2size  29809  upgrewlkle2  29865  wlkl1loop  29896  pthdivtx  29985  2pthnloop  29989  upgrwlkdvde  29995  uhgrwkspthlem2  30012  usgr2pthlem  30021  usgr2pth  30022  clwlkl1loop  30041  crctcshwlkn0lem4  30071  wwlksnextproplem3  30169  wspn0  30182  umgr2adedgwlkonALT  30205  umgr2wlk  30207  umgr2wlkon  30208  elwwlks2  30227  clwwlkccatlem  30249  umgrclwwlkge2  30251  clwlkclwwlklem2  30260  clwlkclwwlkf1lem2  30265  clwlkclwwlkf  30268  clwwlknlbonbgr1  30299  clwwlkn1loopb  30303  clwwlkel  30306  clwwlkext2edg  30316  clwwlknonex2lem2  30368  clwwlknonex2  30369  clwwlknonex2e  30370  1pthon2v  30413  uhgr3cyclex  30442  eupth2lem3lem6  30493  frgr3vlem1  30533  3cyclfrgrrn1  30545  frgrnbnb  30553  frgrwopreglem4a  30570  2clwwlk2clwwlklem  30606  wlkl0  30627  frgrregord013  30655  frgrregord13  30656  frgrogt3nreg  30657  friendship  30659  chcompl  31503  spansncol  31829  hoaddsub  32077  bnj600  35224  sconnpht  35592  satffunlem  35764  satfvel  35775  msubvrs  35923  funpsstri  36129  imp5p  36684  cntotbnd  38307  clmgmOLD  38362  grpomndo  38386  rngoneglmul  38454  rngonegrmul  38455  zerdivemp1x  38458  qmapeldisjsim  39371  rnqmapeleldisjsim  39373  atlex  39952  cvlexch1  39964  cvlsupr4  39981  cvlsupr5  39982  cvlsupr6  39983  2llnneN  40045  athgt  40092  llnle  40154  lplnle  40176  lvoli2  40217  pmaple  40397  dalawlem10  40516  dalawlem13  40519  dalawlem14  40520  dalaw  40522  lhp2lt  40637  ldilval  40749  cdleme50trn2  41187  cdlemf  41199  cdlemg18b  41315  tendotp  41397  tendospcanN  41659  dihmeetlem3N  41941  dvh4dimlem  42079  pell14qrexpclnn0  43455  pell1qrgap  43463  aomclem2  43644  rngunsnply  43758  dflim5  43918  relexpaddss  44306  rp-simp2  44381  gneispaceel2  44732  bi33imp12  45065  bi13imp23  45066  bi23imp1  45069  bi123imp0  45070  ee333  45081  jaoded  45140  e333  45306  suctrALTcf  45495  suctrALTcfVD  45496  ax6e2ndeqALT  45504  mullimc  46190  mullimcf  46197  f1oresf1o2  47883  fzopredsuc  47916  subsubelfzo0  47919  nnmul2b  47923  2tceilhalfelfzo1  47928  2timesltsqm1  47971  muldvdsfacgt  47978  muldvdsfacm1  47979  elsetpreimafvbi  47995  iccpartimp  48021  iccpartigtl  48027  lswn0  48048  poprelb  48128  fmtnofac1  48177  lighneallem2  48213  lighneallem3  48214  lighneallem4  48217  nprmdvdsfacm1lem2  48228  mogoldbblem  48340  fpprel2  48361  gbegt5  48381  sbgoldbaltlem1  48399  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  clnbgrssedg  48461  grimuhgr  48507  uhgrimedgi  48510  uhgrimisgrgriclem  48550  uhgrimisgrgric  48551  clnbgrgrim  48554  grimedg  48555  grimgrtri  48569  usgrgrtrirex  48570  isubgr3stgrlem4  48589  grlimgrtri  48623  clnbgr3stgrgrlim  48639  gpgedgvtx1  48682  gpgvtxedg0  48683  gpgvtxedg1  48684  gpgcubic  48699  gpg5nbgr3star  48701  lidldomn1  48851  cznnring  48882  rngccatidALTV  48892  ringccatidALTV  48926  scmsuppss  49002  lmodvsmdi  49010  gsumlsscl  49011  lindslinindimp2lem1  49089  lindsrng01  49099  elfzolborelfzop1  49150  fllog2  49199  dignn0flhalflem1  49246  rrxlinesc  49366  itschlc0yqe  49391  itsclc0xyqsol  49399  itscnhlinecirc02p  49416