Theorem 3imp 1107

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3imp31  1108  3imp231  1109  3impb  1111  3impib  1112  3imp1  1343  3impd  1344  3jao  1421  biimp3ar  1466  3elpr2eq  4837  wefrc  5549  predpo  6166  iotan0  6345  f1ssf1  6646  fveqdmss  6846  funelss  7746  poxp  7822  fvn0elsuppb  7847  suppfnss  7855  smo11  8001  odi  8205  omass  8206  nndi  8249  nnmass  8250  undifixp  8498  domunfican  8791  preleqg  9078  pr2nelem  9430  dfac8alem  9455  fin33i  9791  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  ttukeyg  9939  axdclem  9941  grupr  10219  nqereu  10351  squeeze0  11543  rpnnen1lem5  12381  xnn0lenn0nn0  12639  supxrun  12710  difelfzle  13021  elfzo0z  13080  fzofzim  13085  fzo1fzo0n0  13089  elfzodifsumelfzo  13104  elfznelfzo  13143  injresinj  13159  mulexp  13469  expadd  13472  expmul  13475  facdiv  13648  hashgt12el2  13785  hashimarni  13803  leisorel  13819  fi1uzind  13856  pfxfv  14044  swrdswrdlem  14066  pfxccat3  14096  reuccatpfxs1lem  14108  repswswrd  14146  cshf1  14172  2cshwcshw  14187  cshimadifsn  14191  relexpindlem  14422  pwdif  15223  dvdsaddre2b  15657  addmodlteqALT  15675  ltoddhalfle  15710  halfleoddlt  15711  coprmprod  16005  coprmproddvds  16007  cncongr1  16011  oddprmgt2  16043  prmfac1  16063  infpnlem1  16246  prmgaplem5  16391  prmgaplem6  16392  cshwshashlem1  16429  setsstruct  16523  iscatd2  16952  initoeu2lem2  17275  clatleglb  17736  dfgrp3e  18199  mulgaddcom  18251  mulginvcom  18252  symgfvne  18509  f1rhm0to0ALT  19494  lsmcv  19913  assamulgscm  20130  psrvscafval  20170  mat1scmat  21148  cramer0  21299  chpscmat  21450  fvmptnn04ifa  21458  fvmptnn04ifc  21460  fvmptnn04ifd  21461  fiinopn  21509  opnneissb  21722  cnpimaex  21864  regsep  21942  hausnei2  21961  cmpsublem  22007  cmpsub  22008  filufint  22528  blssps  23034  blss  23035  mblsplit  24133  bcmono  25853  gausslemma2dlem1a  25941  2sqlem10  26004  elntg2  26771  upgrex  26877  numedglnl  26929  ausgrumgri  26952  ausgrusgri  26953  usgredg2vtxeuALT  27004  ushgredgedg  27011  ushgredgedgloop  27013  edg0usgr  27035  0uhgrsubgr  27061  subumgredg2  27067  fusgrfisbase  27110  cusgrsizeinds  27234  cusgrsize2inds  27235  finsumvtxdg2size  27332  upgrewlkle2  27388  wlkl1loop  27419  pthdivtx  27510  2pthnloop  27512  upgrwlkdvde  27518  uhgrwkspthlem2  27535  usgr2pthlem  27544  usgr2pth  27545  clwlkl1loop  27564  crctcshwlkn0lem4  27591  wwlksnextproplem3  27690  wspn0  27703  umgr2adedgwlkonALT  27726  umgr2wlk  27728  umgr2wlkon  27729  elwwlks2  27745  clwwlkccatlem  27767  umgrclwwlkge2  27769  clwlkclwwlklem2  27778  clwlkclwwlkf1lem2  27783  clwlkclwwlkf  27786  clwwlknlbonbgr1  27817  clwwlkn1loopb  27821  clwwlkel  27825  clwwlkext2edg  27835  clwwlknonex2lem2  27887  clwwlknonex2  27888  clwwlknonex2e  27889  1pthon2v  27932  uhgr3cyclex  27961  eupth2lem3lem6  28012  frgr3vlem1  28052  3cyclfrgrrn1  28064  frgrnbnb  28072  frgrwopreglem4a  28089  2clwwlk2clwwlklem  28125  wlkl0  28146  frgrregord013  28174  frgrregord13  28175  frgrogt3nreg  28176  friendship  28178  chcompl  29019  spansncol  29345  hoaddsub  29593  bnj600  32191  sconnpht  32476  satffunlem  32648  satfvel  32659  msubvrs  32807  funpsstri  33008  imp5p  33659  cntotbnd  35089  clmgmOLD  35144  grpomndo  35168  rngoneglmul  35236  rngonegrmul  35237  zerdivemp1x  35240  atlex  36467  cvlexch1  36479  cvlsupr4  36496  cvlsupr5  36497  cvlsupr6  36498  2llnneN  36560  athgt  36607  llnle  36669  lplnle  36691  lvoli2  36732  pmaple  36912  dalawlem10  37031  dalawlem13  37034  dalawlem14  37035  dalaw  37037  lhp2lt  37152  ldilval  37264  cdleme50trn2  37702  cdlemf  37714  cdlemg18b  37830  tendotp  37912  tendospcanN  38174  dihmeetlem3N  38456  dvh4dimlem  38594  pell14qrexpclnn0  39512  pell1qrgap  39520  aomclem2  39704  rngunsnply  39822  relexpaddss  40112  rp-simp2  40188  gneispaceel2  40543  bi33imp12  40873  bi23imp13  40874  bi13imp23  40875  bi23imp1  40878  bi123imp0  40879  ee333  40890  jaoded  40949  e333  41116  suctrALTcf  41305  suctrALTcfVD  41306  ax6e2ndeqALT  41314  mullimc  41946  mullimcf  41953  f1oresf1o2  43539  fzopredsuc  43572  subsubelfzo0  43575  elsetpreimafvbi  43600  iccpartimp  43626  iccpartigtl  43632  lswn0  43653  poprelb  43735  fmtnofac1  43781  lighneallem2  43820  lighneallem3  43821  lighneallem4  43824  mogoldbblem  43934  fpprel2  43955  gbegt5  43975  sbgoldbaltlem1  43993  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  lidldomn1  44241  cznnring  44276  rngccatidALTV  44309  ringccatidALTV  44372  scmsuppss  44469  lmodvsmdi  44479  gsumlsscl  44480  lindslinindimp2lem1  44562  lindsrng01  44572  elfzolborelfzop1  44623  difmodm1lt  44631  fllog2  44677  dignn0flhalflem1  44724  rrxlinesc  44771  itschlc0yqe  44796  itsclc0xyqsol  44804  itscnhlinecirc02p  44821