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

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  3imp31  1129  3imp231  1130  3impb  1132  bi23imp13  1133  3impib  1134  3imp1  1366  3impd  1367  3jao  1452  biimp3ar  1499  3elpr2eq  4872  wefrc  5657  iotan0  6528  f1ssf1  6855  fveqdmss  7075  funelss  8045  poxp  8125  fvn0elsuppb  8178  suppfnss  8186  smo11  8352  odi  8565  omass  8566  nndi  8610  nnmass  8611  undifixp  8933  domunfican  9282  preleqg  9585  dfac8alem  10014  fin33i  10354  domtriomlem  10427  axdc3lem2  10436  axdc3lem4  10438  axdc4lem  10440  ttukeyg  10502  axdclem  10504  grupr  10783  nqereu  10915  squeeze0  12119  rpnnen1lem5  13006  xnn0lenn0nn0  13272  supxrun  13343  difelfzle  13671  elfzo0z  13732  fzofzim  13740  fzo1fzo0n0  13746  elfzodifsumelfzo  13762  elfznelfzo  13804  injresinj  13822  mulexp  14139  expadd  14142  expmul  14145  facdiv  14325  hashgt12el2  14462  hashimarni  14480  leisorel  14499  fi1uzind  14546  pfxfv  14722  swrdswrdlem  14743  pfxccat3  14773  reuccatpfxs1lem  14785  repswswrd  14823  cshf1  14849  2cshwcshw  14864  cshimadifsn  14868  relexpindlem  15102  pwdif  15924  dvdsaddre2b  16366  addmodlteqALT  16384  ltoddhalfle  16420  halfleoddlt  16421  coprmprod  16720  coprmproddvds  16722  cncongr1  16726  oddprmgt2  16759  prmfac1  16780  infpnlem1  16971  prmgaplem5  17116  prmgaplem6  17117  cshwshashlem1  17156  setsstruct  17237  iscatd2  17738  initoeu2lem2  18073  clatleglb  18575  dfgrp3e  19107  mulgaddcom  19165  mulginvcom  19166  symgfvne  19452  lsmcv  21246  lidlunin0  21342  assamulgscm  22032  psrvscafval  22079  mat1scmat  22677  cramer0  22828  chpscmat  22980  fvmptnn04ifa  22988  fvmptnn04ifc  22990  fvmptnn04ifd  22991  fiinopn  23039  opnneissb  23252  cnpimaex  23394  regsep  23472  hausnei2  23491  cmpsublem  23537  cmpsub  23538  filufint  24058  blssps  24562  blss  24563  mblsplit  25672  dvply2g  26427  taylply2  26509  bcmono  27419  gausslemma2dlem1a  27507  2sqlem10  27570  eqcuts3  27975  addsuniflem  28172  negsunif  28226  sltmuls2  28319  precsexlem11  28388  bdaypw2n0bndlem  28634  elreno2  28666  elntg2  29313  upgrex  29420  numedglnl  29472  ausgrumgri  29495  ausgrusgri  29496  usgredg2vtxeuALT  29550  ushgredgedg  29557  ushgredgedgloop  29559  edg0usgr  29581  0uhgrsubgr  29607  subumgredg2  29613  fusgrfisbase  29656  cusgrsizeinds  29780  cusgrsize2inds  29781  finsumvtxdg2size  29878  upgrewlkle2  29934  wlkl1loop  29965  pthdivtx  30054  2pthnloop  30058  upgrwlkdvde  30064  uhgrwkspthlem2  30081  usgr2pthlem  30090  usgr2pth  30091  clwlkl1loop  30110  crctcshwlkn0lem4  30140  wwlksnextproplem3  30238  wspn0  30251  umgr2adedgwlkonALT  30274  umgr2wlk  30276  umgr2wlkon  30277  elwwlks2  30296  clwwlkccatlem  30318  umgrclwwlkge2  30320  clwlkclwwlklem2  30329  clwlkclwwlkf1lem2  30334  clwlkclwwlkf  30337  clwwlknlbonbgr1  30368  clwwlkn1loopb  30372  clwwlkel  30375  clwwlkext2edg  30385  clwwlknonex2lem2  30437  clwwlknonex2  30438  clwwlknonex2e  30439  1pthon2v  30482  uhgr3cyclex  30511  eupth2lem3lem6  30562  frgr3vlem1  30602  3cyclfrgrrn1  30614  frgrnbnb  30622  frgrwopreglem4a  30639  2clwwlk2clwwlklem  30675  wlkl0  30696  frgrregord013  30724  frgrregord13  30725  frgrogt3nreg  30726  friendship  30728  chcompl  31572  spansncol  31898  hoaddsub  32146  bnj600  35285  sconnpht  35699  satffunlem  35871  satfvel  35882  msubvrs  36030  funpsstri  36236  imp5p  36801  cntotbnd  38425  clmgmOLD  38480  grpomndo  38504  rngoneglmul  38572  rngonegrmul  38573  zerdivemp1x  38576  qmapeldisjsim  39487  rnqmapeleldisjsim  39489  atlex  40068  cvlexch1  40080  cvlsupr4  40097  cvlsupr5  40098  cvlsupr6  40099  2llnneN  40161  athgt  40208  llnle  40270  lplnle  40292  lvoli2  40333  pmaple  40513  dalawlem10  40632  dalawlem13  40635  dalawlem14  40636  dalaw  40638  lhp2lt  40753  ldilval  40865  cdleme50trn2  41303  cdlemf  41315  cdlemg18b  41431  tendotp  41513  tendospcanN  41775  dihmeetlem3N  42057  dvh4dimlem  42195  pell14qrexpclnn0  43573  pell1qrgap  43581  aomclem2  43762  rngunsnply  43876  dflim5  44036  relexpaddss  44424  rp-simp2  44499  gneispaceel2  44850  bi33imp12  45180  bi13imp23  45181  bi23imp1  45184  bi123imp0  45185  ee333  45196  jaoded  45255  e333  45421  suctrALTcf  45610  suctrALTcfVD  45611  ax6e2ndeqALT  45619  mullimc  46312  mullimcf  46319  f1oresf1o2  48005  fzopredsuc  48038  subsubelfzo0  48041  nnmul2b  48045  2tceilhalfelfzo1  48050  2timesltsqm1  48093  muldvdsfacgt  48100  muldvdsfacm1  48101  elsetpreimafvbi  48117  iccpartimp  48143  iccpartigtl  48149  lswn0  48170  poprelb  48250  fmtnofac1  48299  lighneallem2  48335  lighneallem3  48336  lighneallem4  48339  nprmdvdsfacm1lem2  48350  mogoldbblem  48462  fpprel2  48483  gbegt5  48503  sbgoldbaltlem1  48521  bgoldbtbndlem2  48548  bgoldbtbndlem3  48549  clnbgrssedg  48583  grimuhgr  48629  uhgrimedgi  48632  uhgrimisgrgriclem  48672  uhgrimisgrgric  48673  clnbgrgrim  48676  grimedg  48677  grimgrtri  48691  usgrgrtrirex  48692  isubgr3stgrlem4  48711  grlimgrtri  48745  clnbgr3stgrgrlim  48761  gpgedgvtx1  48804  gpgvtxedg0  48805  gpgvtxedg1  48806  gpgcubic  48821  gpg5nbgr3star  48823  lidldomn1  48973  cznnring  49004  rngccatidALTV  49014  ringccatidALTV  49048  scmsuppss  49128  lmodvsmdi  49136  gsumlsscl  49137  lindslinindimp2lem1  49215  lindsrng01  49225  elfzolborelfzop1  49276  fllog2  49325  dignn0flhalflem1  49372  rrxlinesc  49492  itschlc0yqe  49517  itsclc0xyqsol  49525  itscnhlinecirc02p  49542