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  4876  wefrc  5660  iotan0  6533  f1ssf1  6860  fveqdmss  7080  funelss  8053  poxp  8133  fvn0elsuppb  8186  suppfnss  8194  smo11  8360  odi  8573  omass  8574  nndi  8618  nnmass  8619  undifixp  8941  domunfican  9291  preleqg  9594  dfac8alem  10032  fin33i  10371  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  ttukeyg  10519  axdclem  10521  grupr  10800  nqereu  10932  squeeze0  12136  rpnnen1lem5  13023  xnn0lenn0nn0  13289  supxrun  13360  difelfzle  13688  elfzo0z  13749  fzofzim  13757  fzo1fzo0n0  13763  elfzodifsumelfzo  13779  elfznelfzo  13821  injresinj  13839  mulexp  14157  expadd  14160  expmul  14163  facdiv  14343  hashgt12el2  14480  hashimarni  14498  leisorel  14517  fi1uzind  14564  pfxfv  14744  swrdswrdlem  14765  pfxccat3  14795  reuccatpfxs1lem  14807  repswswrd  14847  cshf1  14873  2cshwcshw  14888  cshimadifsn  14892  relexpindlem  15126  pwdif  15948  dvdsaddre2b  16390  addmodlteqALT  16408  ltoddhalfle  16444  halfleoddlt  16445  coprmprod  16744  coprmproddvds  16746  cncongr1  16750  oddprmgt2  16783  prmfac1  16804  infpnlem1  16995  prmgaplem5  17140  prmgaplem6  17141  cshwshashlem1  17180  setsstruct  17261  iscatd2  17762  initoeu2lem2  18097  clatleglb  18599  dfgrp3e  19137  mulgaddcom  19195  mulginvcom  19196  symgfvne  19482  isdrng3lem2  20889  lsmcv  21302  lidlunin0  21398  assamulgscm  22088  psrvscafval  22135  mat1scmat  22733  cramer0  22884  chpscmat  23036  fvmptnn04ifa  23044  fvmptnn04ifc  23046  fvmptnn04ifd  23047  fiinopn  23095  opnneissb  23308  cnpimaex  23450  regsep  23528  hausnei2  23547  cmpsublem  23593  cmpsub  23594  filufint  24114  blssps  24618  blss  24619  mblsplit  25728  dvply2g  26483  taylply2  26568  bcmono  27478  gausslemma2dlem1a  27566  2sqlem10  27629  eqcuts3  28034  addsuniflem  28231  negsunif  28285  sltmuls2  28378  precsexlem11  28447  bdaypw2n0bndlem  28693  elreno2  28725  elntg2  29372  upgrex  29479  numedglnl  29531  ausgrumgri  29554  ausgrusgri  29555  usgredg2vtxeuALT  29609  ushgredgedg  29616  ushgredgedgloop  29618  edg0usgr  29640  0uhgrsubgr  29666  subumgredg2  29672  fusgrfisbase  29715  cusgrsizeinds  29839  cusgrsize2inds  29840  finsumvtxdg2size  29937  upgrewlkle2  29993  wlkl1loop  30024  pthdivtx  30113  2pthnloop  30117  upgrwlkdvde  30123  uhgrwkspthlem2  30140  usgr2pthlem  30149  usgr2pth  30150  clwlkl1loop  30169  crctcshwlkn0lem4  30199  wwlksnextproplem3  30297  wspn0  30310  umgr2adedgwlkonALT  30333  umgr2wlk  30335  umgr2wlkon  30336  elwwlks2  30355  clwwlkccatlem  30377  umgrclwwlkge2  30379  clwlkclwwlklem2  30388  clwlkclwwlkf1lem2  30393  clwlkclwwlkf  30396  clwwlknlbonbgr1  30427  clwwlkn1loopb  30431  clwwlkel  30434  clwwlkext2edg  30444  clwwlknonex2lem2  30496  clwwlknonex2  30497  clwwlknonex2e  30498  1pthon2v  30541  uhgr3cyclex  30570  eupth2lem3lem6  30621  frgr3vlem1  30661  3cyclfrgrrn1  30673  frgrnbnb  30681  frgrwopreglem4a  30698  2clwwlk2clwwlklem  30734  wlkl0  30755  frgrregord013  30783  frgrregord13  30784  frgrogt3nreg  30785  friendship  30787  chcompl  31631  spansncol  31957  hoaddsub  32205  bnj600  35338  sconnpht  35741  satffunlem  35913  satfvel  35924  msubvrs  36072  funpsstri  36278  imp5p  36863  cntotbnd  38487  clmgmOLD  38542  grpomndo  38566  rngoneglmul  38634  rngonegrmul  38635  zerdivemp1x  38638  qmapeldisjsim  39549  rnqmapeleldisjsim  39551  atlex  40130  cvlexch1  40142  cvlsupr4  40159  cvlsupr5  40160  cvlsupr6  40161  2llnneN  40223  athgt  40270  llnle  40332  lplnle  40354  lvoli2  40395  pmaple  40575  dalawlem10  40694  dalawlem13  40697  dalawlem14  40698  dalaw  40700  lhp2lt  40815  ldilval  40927  cdleme50trn2  41365  cdlemf  41377  cdlemg18b  41493  tendotp  41575  tendospcanN  41837  dihmeetlem3N  42119  dvh4dimlem  42257  pell14qrexpclnn0  43633  pell1qrgap  43641  aomclem2  43822  rngunsnply  43936  dflim5  44096  relexpaddss  44484  rp-simp2  44559  gneispaceel2  44910  bi33imp12  45240  bi13imp23  45241  bi23imp1  45244  bi123imp0  45245  ee333  45256  jaoded  45315  e333  45481  suctrALTcf  45670  suctrALTcfVD  45671  ax6e2ndeqALT  45679  mullimc  46372  mullimcf  46379  f1oresf1o2  48068  fzopredsuc  48101  subsubelfzo0  48104  nnmul2b  48108  2tceilhalfelfzo1  48113  2timesltsqm1  48156  muldvdsfacgt  48163  muldvdsfacm1  48164  elsetpreimafvbi  48180  iccpartimp  48206  iccpartigtl  48212  lswn0  48233  poprelb  48313  fmtnofac1  48362  lighneallem2  48398  lighneallem3  48399  lighneallem4  48402  nprmdvdsfacm1lem2  48413  mogoldbblem  48525  fpprel2  48546  gbegt5  48566  sbgoldbaltlem1  48584  bgoldbtbndlem2  48611  bgoldbtbndlem3  48612  clnbgrssedg  48646  grimuhgr  48692  uhgrimedgi  48695  uhgrimisgrgriclem  48735  uhgrimisgrgric  48736  clnbgrgrim  48739  grimedg  48740  grimgrtri  48754  usgrgrtrirex  48755  isubgr3stgrlem4  48774  grlimgrtri  48808  clnbgr3stgrgrlim  48824  gpgedgvtx1  48867  gpgvtxedg0  48868  gpgvtxedg1  48869  gpgcubic  48884  gpg5nbgr3star  48886  lidldomn1  49036  cznnring  49067  rngccatidALTV  49077  ringccatidALTV  49111  scmsuppss  49191  lmodvsmdi  49199  gsumlsscl  49200  lindslinindimp2lem1  49278  lindsrng01  49288  elfzolborelfzop1  49339  fllog2  49388  dignn0flhalflem1  49435  rrxlinesc  49555  itschlc0yqe  49580  itsclc0xyqsol  49588  itscnhlinecirc02p  49605