Theorem 3imp 1128

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3imp31  1129  3imp231  1130  3impb  1132  bi23imp13  1133  3impib  1134  3imp1  1366  3impd  1367  3jao  1452  biimp3ar  1499  3elpr2eq  4869  wefrc  5653  iotan0  6527  f1ssf1  6854  fveqdmss  7075  funelss  8048  poxp  8130  fvn0elsuppb  8183  suppfnss  8191  smo11  8357  odi  8570  omass  8571  nndi  8615  nnmass  8616  undifixp  8945  domunfican  9295  preleqg  9598  dfac8alem  10036  fin33i  10375  domtriomlem  10448  axdc3lem2  10457  axdc3lem4  10459  axdc4lem  10461  ttukeyg  10523  axdclem  10525  grupr  10810  nqereu  10942  squeeze0  12146  rpnnen1lem5  13035  xnn0lenn0nn0  13301  supxrun  13372  difelfzle  13700  elfzo0z  13761  fzofzim  13769  fzo1fzo0n0  13775  elfzodifsumelfzo  13791  elfznelfzo  13833  injresinj  13851  mulexp  14169  expadd  14172  expmul  14175  facdiv  14355  hashgt12el2  14492  hashimarni  14510  leisorel  14529  fi1uzind  14576  pfxfv  14756  swrdswrdlem  14777  pfxccat3  14807  reuccatpfxs1lem  14819  repswswrd  14859  cshf1  14885  2cshwcshw  14900  cshimadifsn  14904  relexpindlem  15140  pwdif  15961  dvdsaddre2b  16403  addmodlteqALT  16421  ltoddhalfle  16457  halfleoddlt  16458  coprmprod  16757  coprmproddvds  16759  cncongr1  16763  oddprmgt2  16796  prmfac1  16817  infpnlem1  17008  prmgaplem5  17153  prmgaplem6  17154  cshwshashlem1  17193  setsstruct  17274  iscatd2  17775  initoeu2lem2  18110  clatleglb  18612  dfgrp3e  19169  mulgaddcom  19227  mulginvcom  19228  symgfvne  19514  isdrng3lem2  20921  lsmcv  21334  lidlunin0  21430  assamulgscm  22122  psrvscafval  22169  mat1scmat  22767  cramer0  22921  chpscmat  23073  fvmptnn04ifa  23081  fvmptnn04ifc  23083  fvmptnn04ifd  23084  fiinopn  23132  opnneissb  23345  cnpimaex  23487  regsep  23565  hausnei2  23584  cmpsublem  23630  cmpsub  23631  filufint  24152  blssps  24656  blss  24657  mblsplit  25766  dvply2g  26522  taylply2  26611  bcmono  27521  gausslemma2dlem1a  27609  2sqlem10  27672  eqcuts3  28077  addsuniflem  28274  negsunif  28328  sltmuls2  28421  precsexlem11  28490  bdaypw2n0bndlem  28736  elreno2  28768  elntg2  29450  upgrex  29557  numedglnl  29609  ausgrumgri  29635  ausgrusgri  29636  usgredg2vtxeuALT  29690  ushgredgedg  29697  ushgredgedgloop  29699  edg0usgr  29721  0uhgrsubgr  29747  subumgredg2  29753  fusgrfisbase  29796  cusgrsizeinds  29920  cusgrsize2inds  29921  finsumvtxdg2size  30018  upgrewlkle2  30074  wlkl1loop  30105  pthdivtx  30199  2pthnloop  30204  upgrwlkdvde  30210  uhgrwkspthlem2  30227  usgr2pthlem  30236  usgr2pth  30237  clwlkl1loop  30257  crctcshwlkn0lem4  30289  wwlksnextproplem3  30387  wspn0  30400  umgr2adedgwlkonALT  30423  umgr2wlk  30425  umgr2wlkon  30426  elwwlks2  30445  clwwlkccatlem  30467  umgrclwwlkge2  30469  clwlkclwwlklem2  30478  clwlkclwwlkf1lem2  30483  clwlkclwwlkf  30486  clwwlknlbonbgr1  30517  clwwlkn1loopb  30521  clwwlkel  30524  clwwlkext2edg  30534  clwwlknonex2lem2  30586  clwwlknonex2  30587  clwwlknonex2e  30588  1pthon2v  30641  uhgr3cyclex  30670  eupth2lem3lem6  30721  frgr3vlem1  30761  3cyclfrgrrn1  30773  frgrnbnb  30781  frgrwopreglem4a  30798  2clwwlk2clwwlklem  30834  wlkl0  30855  frgrregord013  30883  frgrregord13  30884  frgrogt3nreg  30885  friendship  30887  chcompl  31731  spansncol  32057  hoaddsub  32305  bnj600  35436  sconnpht  35816  satffunlem  35988  satfvel  35999  msubvrs  36147  funpsstri  36353  imp5p  36939  cntotbnd  38554  clmgmOLD  38609  grpomndo  38633  rngoneglmul  38701  rngonegrmul  38702  zerdivemp1x  38705  qmapeldisjsim  39616  rnqmapeleldisjsim  39618  atlex  40197  cvlexch1  40209  cvlsupr4  40226  cvlsupr5  40227  cvlsupr6  40228  2llnneN  40290  athgt  40337  llnle  40399  lplnle  40421  lvoli2  40462  pmaple  40642  dalawlem10  40761  dalawlem13  40764  dalawlem14  40765  dalaw  40767  lhp2lt  40882  ldilval  40994  cdleme50trn2  41432  cdlemf  41444  cdlemg18b  41560  tendotp  41642  tendospcanN  41904  dihmeetlem3N  42186  dvh4dimlem  42324  pell14qrexpclnn0  43715  pell1qrgap  43723  aomclem2  43904  rngunsnply  44018  dflim5  44178  relexpaddss  44566  rp-simp2  44641  gneispaceel2  44992  bi33imp12  45322  bi13imp23  45323  bi23imp1  45326  bi123imp0  45327  ee333  45338  jaoded  45397  e333  45563  suctrALTcf  45752  suctrALTcfVD  45753  ax6e2ndeqALT  45761  mullimc  46454  mullimcf  46461  f1oresf1o2  48187  fzopredsuc  48220  subsubelfzo0  48223  nnmul2b  48227  2tceilhalfelfzo1  48232  2timesltsqm1  48275  muldvdsfacgt  48282  muldvdsfacm1  48283  elsetpreimafvbi  48299  iccpartimp  48325  iccpartigtl  48331  lswn0  48352  poprelb  48432  fmtnofac1  48481  lighneallem2  48517  lighneallem3  48518  lighneallem4  48521  nprmdvdsfacm1lem2  48532  mogoldbblem  48644  fpprel2  48665  gbegt5  48685  sbgoldbaltlem1  48703  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  clnbgrssedg  48765  grimuhgr  48811  uhgrimedgi  48814  uhgrimisgrgriclem  48854  uhgrimisgrgric  48855  clnbgrgrim  48858  grimedg  48859  grimgrtri  48873  usgrgrtrirex  48874  isubgr3stgrlem4  48893  grlimgrtri  48927  clnbgr3stgrgrlim  48943  gpgedgvtx1  48986  gpgvtxedg0  48987  gpgvtxedg1  48988  gpgcubic  49003  gpg5nbgr3star  49005  lidldomn1  49154  cznnring  49185  rngccatidALTV  49195  ringccatidALTV  49229  scmsuppss  49309  lmodvsmdi  49317  gsumlsscl  49318  lindslinindimp2lem1  49396  lindsrng01  49406  elfzolborelfzop1  49457  fllog2  49506  dignn0flhalflem1  49553  rrxlinesc  49673  itschlc0yqe  49698  itsclc0xyqsol  49706  itscnhlinecirc02p  49723