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  1453  biimp3ar  1500  3elpr2eq  4837  wefrc  5649  iotan0OLD  6548  f1ssf1  6880  fveqdmss  7102  funelss  8083  poxp  8167  fvn0elsuppb  8226  suppfnss  8234  smo11  8400  odi  8615  omass  8616  nndi  8660  nnmass  8661  undifixp  8990  domunfican  9341  preleqg  9643  dfac8alem  10135  fin33i  10474  domtriomlem  10547  axdc3lem2  10556  axdc3lem4  10558  axdc4lem  10560  ttukeyg  10622  axdclem  10624  grupr  10909  nqereu  11041  squeeze0  12247  rpnnen1lem5  13136  xnn0lenn0nn0  13402  supxrun  13473  difelfzle  13802  elfzo0z  13863  fzofzim  13871  fzo1fzo0n0  13877  elfzodifsumelfzo  13893  elfznelfzo  13935  injresinj  13953  mulexp  14271  expadd  14274  expmul  14277  facdiv  14458  hashgt12el2  14595  hashimarni  14613  leisorel  14632  fi1uzind  14679  pfxfv  14860  swrdswrdlem  14881  pfxccat3  14911  reuccatpfxs1lem  14923  repswswrd  14963  cshf1  14989  2cshwcshw  15004  cshimadifsn  15008  relexpindlem  15245  pwdif  16066  dvdsaddre2b  16506  addmodlteqALT  16524  ltoddhalfle  16560  halfleoddlt  16561  coprmprod  16865  coprmproddvds  16867  cncongr1  16871  oddprmgt2  16904  prmfac1  16925  infpnlem1  17117  prmgaplem5  17262  prmgaplem6  17263  cshwshashlem1  17302  setsstruct  17383  iscatd2  17884  initoeu2lem2  18219  clatleglb  18721  dfgrp3e  19279  mulgaddcom  19337  mulginvcom  19338  symgfvne  19625  isdrng3lem2  21036  lsmcv  21449  lidlunin0  21545  assamulgscm  22239  psrvscafval  22286  mat1scmat  22884  cramer0  23038  chpscmat  23190  fvmptnn04ifa  23198  fvmptnn04ifc  23200  fvmptnn04ifd  23201  fiinopn  23249  opnneissb  23462  cnpimaex  23604  regsep  23682  hausnei2  23701  cmpsublem  23747  cmpsub  23748  filufint  24269  blssps  24773  blss  24774  mblsplit  25883  dvply2g  26636  taylply2  26725  bcmono  27634  gausslemma2dlem1a  27722  2sqlem10  27785  fltoprmlem2  28024  eqcuts3  28220  addsuniflem  28417  negsunif  28471  sltmuls2  28564  precsexlem11  28633  bdaypw2n0bndlem  28879  elreno2  28911  elntg2  29593  upgrex  29700  numedglnl  29752  ausgrumgri  29778  ausgrusgri  29779  usgredg2vtxeuALT  29833  ushgredgedg  29840  ushgredgedgloop  29842  edg0usgr  29864  0uhgrsubgr  29890  subumgredg2  29896  fusgrfisbase  29939  cusgrsizeinds  30063  cusgrsize2inds  30064  finsumvtxdg2size  30161  upgrewlkle2  30217  wlkl1loop  30248  pthdivtx  30342  2pthnloop  30347  upgrwlkdvde  30353  uhgrwkspthlem2  30370  usgr2pthlem  30379  usgr2pth  30380  clwlkl1loop  30400  crctcshwlkn0lem4  30432  wwlksnextproplem3  30530  wspn0  30543  umgr2adedgwlkonALT  30566  umgr2wlk  30568  umgr2wlkon  30569  elwwlks2  30588  clwwlkccatlem  30610  umgrclwwlkge2  30612  clwlkclwwlklem2  30621  clwlkclwwlkf1lem2  30626  clwlkclwwlkf  30629  clwwlknlbonbgr1  30660  clwwlkn1loopb  30664  clwwlkel  30667  clwwlkext2edg  30677  clwwlknonex2lem2  30729  clwwlknonex2  30730  clwwlknonex2e  30731  1pthon2v  30784  uhgr3cyclex  30813  eupth2lem3lem6  30864  frgr3vlem1  30904  3cyclfrgrrn1  30916  frgrnbnb  30924  frgrwopreglem4a  30941  2clwwlk2clwwlklem  30977  wlkl0  30998  frgrregord013  31026  frgrregord13  31027  frgrogt3nreg  31028  friendship  31030  chcompl  31874  spansncol  32200  hoaddsub  32448  bnj600  35619  sconnpht  36161  satffunlem  36333  satfvel  36344  msubvrs  36492  funpsstri  36709  imp5p  37278  cntotbnd  38922  clmgmOLD  38977  grpomndo  39001  rngoneglmul  39069  rngonegrmul  39070  zerdivemp1x  39073  qmapeldisjsim  39984  rnqmapeleldisjsim  39986  atlex  40565  cvlexch1  40577  cvlsupr4  40594  cvlsupr5  40595  cvlsupr6  40596  2llnneN  40658  athgt  40705  llnle  40767  lplnle  40789  lvoli2  40830  pmaple  41010  dalawlem10  41129  dalawlem13  41132  dalawlem14  41133  dalaw  41135  lhp2lt  41250  ldilval  41362  cdleme50trn2  41800  cdlemf  41812  cdlemg18b  41928  tendotp  42010  tendospcanN  42272  dihmeetlem3N  42554  dvh4dimlem  42692  pell14qrexpclnn0  44066  pell1qrgap  44074  aomclem2  44250  rngunsnply  44363  dflim5  44523  relexpaddss  44910  rp-simp2  44985  gneispaceel2  45336  bi33imp12  45665  bi13imp23  45666  bi23imp1  45669  bi123imp0  45670  ee333  45681  jaoded  45740  e333  45906  suctrALTcf  46095  suctrALTcfVD  46096  ax6e2ndeqALT  46104  mullimc  46833  mullimcf  46840  f1oresf1o2  48566  fzopredsuc  48599  subsubelfzo0  48602  nnmul2b  48606  2tceilhalfelfzo1  48611  2timesltsqm1  48654  muldvdsfacgt  48661  muldvdsfacm1  48662  elsetpreimafvbi  48678  iccpartimp  48704  iccpartigtl  48710  lswn0  48731  poprelb  48811  fmtnofac1  48860  lighneallem2  48896  lighneallem3  48897  lighneallem4  48900  nprmdvdsfacm1lem2  48911  mogoldbblem  49023  fpprel2  49044  gbegt5  49064  sbgoldbaltlem1  49082  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  clnbgrssedg  49144  grimuhgr  49190  uhgrimedgi  49193  uhgrimisgrgriclem  49233  uhgrimisgrgric  49234  clnbgrgrim  49237  grimedg  49238  grimgrtri  49252  usgrgrtrirex  49253  isubgr3stgrlem4  49272  grlimgrtri  49306  clnbgr3stgrgrlim  49322  gpgedgvtx1  49365  gpgvtxedg0  49366  gpgvtxedg1  49367  gpgcubic  49382  gpg5nbgr3star  49384  lidldomn1  49533  cznnring  49564  rngccatidALTV  49574  ringccatidALTV  49608  scmsuppss  49688  lmodvsmdi  49696  gsumlsscl  49697  lindslinindimp2lem1  49775  lindsrng01  49785  elfzolborelfzop1  49836  fllog2  49885  dignn0flhalflem1  49932  rrxlinesc  50053  itschlc0yqe  50077  itsclc0xyqsol  50085