Theorem 3imp 1116

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3imp31  1117  3imp231  1118  3impb  1120  bi23imp13  1121  3impib  1122  3imp1  1354  3impd  1355  3jao  1433  biimp3ar  1478  3elpr2eq  4844  wefrc  5619  iotan0  6482  f1ssf1  6806  fveqdmss  7026  funelss  7996  poxp  8075  fvn0elsuppb  8128  suppfnss  8136  smo11  8301  odi  8511  omass  8512  nndi  8556  nnmass  8557  undifixp  8879  domunfican  9229  preleqg  9534  dfac8alem  9949  fin33i  10289  domtriomlem  10362  axdc3lem2  10371  axdc3lem4  10373  axdc4lem  10375  ttukeyg  10437  axdclem  10439  grupr  10718  nqereu  10850  squeeze0  12057  rpnnen1lem5  12929  xnn0lenn0nn0  13195  supxrun  13266  difelfzle  13593  elfzo0z  13654  fzofzim  13662  fzo1fzo0n0  13668  elfzodifsumelfzo  13684  elfznelfzo  13726  injresinj  13744  mulexp  14061  expadd  14064  expmul  14067  facdiv  14247  hashgt12el2  14383  hashimarni  14401  leisorel  14420  fi1uzind  14467  pfxfv  14643  swrdswrdlem  14664  pfxccat3  14694  reuccatpfxs1lem  14706  repswswrd  14744  cshf1  14770  2cshwcshw  14785  cshimadifsn  14789  relexpindlem  15023  pwdif  15831  dvdsaddre2b  16274  addmodlteqALT  16292  ltoddhalfle  16328  halfleoddlt  16329  coprmprod  16628  coprmproddvds  16630  cncongr1  16634  oddprmgt2  16667  prmfac1  16688  infpnlem1  16879  prmgaplem5  17024  prmgaplem6  17025  cshwshashlem1  17064  setsstruct  17144  iscatd2  17645  initoeu2lem2  17980  clatleglb  18482  dfgrp3e  19014  mulgaddcom  19072  mulginvcom  19073  symgfvne  19354  lsmcv  21141  assamulgscm  21883  psrvscafval  21930  mat1scmat  22529  cramer0  22680  chpscmat  22832  fvmptnn04ifa  22840  fvmptnn04ifc  22842  fvmptnn04ifd  22843  fiinopn  22891  opnneissb  23104  cnpimaex  23246  regsep  23324  hausnei2  23343  cmpsublem  23389  cmpsub  23390  filufint  23910  blssps  24414  blss  24415  mblsplit  25524  dvply2g  26276  taylply2  26358  bcmono  27265  gausslemma2dlem1a  27353  2sqlem10  27416  eqcuts3  27821  addsuniflem  28018  negsunif  28072  sltmuls2  28165  precsexlem11  28234  bdaypw2n0bndlem  28480  elreno2  28512  elntg2  29079  upgrex  29186  numedglnl  29238  ausgrumgri  29261  ausgrusgri  29262  usgredg2vtxeuALT  29316  ushgredgedg  29323  ushgredgedgloop  29325  edg0usgr  29347  0uhgrsubgr  29373  subumgredg2  29379  fusgrfisbase  29422  cusgrsizeinds  29546  cusgrsize2inds  29547  finsumvtxdg2size  29644  upgrewlkle2  29700  wlkl1loop  29731  pthdivtx  29820  2pthnloop  29824  upgrwlkdvde  29830  uhgrwkspthlem2  29847  usgr2pthlem  29856  usgr2pth  29857  clwlkl1loop  29876  crctcshwlkn0lem4  29906  wwlksnextproplem3  30004  wspn0  30017  umgr2adedgwlkonALT  30040  umgr2wlk  30042  umgr2wlkon  30043  elwwlks2  30062  clwwlkccatlem  30084  umgrclwwlkge2  30086  clwlkclwwlklem2  30095  clwlkclwwlkf1lem2  30100  clwlkclwwlkf  30103  clwwlknlbonbgr1  30134  clwwlkn1loopb  30138  clwwlkel  30141  clwwlkext2edg  30151  clwwlknonex2lem2  30203  clwwlknonex2  30204  clwwlknonex2e  30205  1pthon2v  30248  uhgr3cyclex  30277  eupth2lem3lem6  30328  frgr3vlem1  30368  3cyclfrgrrn1  30380  frgrnbnb  30388  frgrwopreglem4a  30405  2clwwlk2clwwlklem  30441  wlkl0  30462  frgrregord013  30490  frgrregord13  30491  frgrogt3nreg  30492  friendship  30494  chcompl  31338  spansncol  31664  hoaddsub  31912  bnj600  35108  sconnpht  35464  satffunlem  35636  satfvel  35647  msubvrs  35795  funpsstri  36001  imp5p  36546  cntotbnd  38170  clmgmOLD  38225  grpomndo  38249  rngoneglmul  38317  rngonegrmul  38318  zerdivemp1x  38321  qmapeldisjsim  39234  rnqmapeleldisjsim  39236  atlex  39815  cvlexch1  39827  cvlsupr4  39844  cvlsupr5  39845  cvlsupr6  39846  2llnneN  39908  athgt  39955  llnle  40017  lplnle  40039  lvoli2  40080  pmaple  40260  dalawlem10  40379  dalawlem13  40382  dalawlem14  40383  dalaw  40385  lhp2lt  40500  ldilval  40612  cdleme50trn2  41050  cdlemf  41062  cdlemg18b  41178  tendotp  41260  tendospcanN  41522  dihmeetlem3N  41804  dvh4dimlem  41942  pell14qrexpclnn0  43318  pell1qrgap  43326  aomclem2  43507  rngunsnply  43621  dflim5  43781  relexpaddss  44169  rp-simp2  44244  gneispaceel2  44595  bi33imp12  44942  bi13imp23  44943  bi23imp1  44946  bi123imp0  44947  ee333  44958  jaoded  45017  e333  45183  suctrALTcf  45372  suctrALTcfVD  45373  ax6e2ndeqALT  45381  mullimc  46068  mullimcf  46075  f1oresf1o2  47761  fzopredsuc  47794  subsubelfzo0  47797  nnmul2b  47801  2tceilhalfelfzo1  47806  2timesltsqm1  47849  muldvdsfacgt  47856  muldvdsfacm1  47857  elsetpreimafvbi  47873  iccpartimp  47899  iccpartigtl  47905  lswn0  47926  poprelb  48006  fmtnofac1  48055  lighneallem2  48091  lighneallem3  48092  lighneallem4  48095  nprmdvdsfacm1lem2  48106  mogoldbblem  48218  fpprel2  48239  gbegt5  48259  sbgoldbaltlem1  48277  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  clnbgrssedg  48339  grimuhgr  48385  uhgrimedgi  48388  uhgrimisgrgriclem  48428  uhgrimisgrgric  48429  clnbgrgrim  48432  grimedg  48433  grimgrtri  48447  usgrgrtrirex  48448  isubgr3stgrlem4  48467  grlimgrtri  48501  clnbgr3stgrgrlim  48517  gpgedgvtx1  48560  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgcubic  48577  gpg5nbgr3star  48579  lidldomn1  48729  cznnring  48760  rngccatidALTV  48770  ringccatidALTV  48804  scmsuppss  48869  lmodvsmdi  48877  gsumlsscl  48878  lindslinindimp2lem1  48956  lindsrng01  48966  elfzolborelfzop1  49017  fllog2  49066  dignn0flhalflem1  49113  rrxlinesc  49233  itschlc0yqe  49258  itsclc0xyqsol  49266  itscnhlinecirc02p  49283