Theorem 3imp 1109

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3imp31  1110  3imp231  1111  3impb  1113  3impib  1114  3imp1  1345  3impd  1346  3jao  1423  biimp3ar  1468  3elpr2eq  4835  wefrc  5574  iotan0  6408  f1ssf1  6731  fveqdmss  6938  funelss  7861  poxp  7940  fvn0elsuppb  7968  suppfnss  7976  smo11  8166  odi  8372  omass  8373  nndi  8416  nnmass  8417  undifixp  8680  domunfican  9017  preleqg  9303  pr2nelem  9691  dfac8alem  9716  fin33i  10056  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  ttukeyg  10204  axdclem  10206  grupr  10484  nqereu  10616  squeeze0  11808  rpnnen1lem5  12650  xnn0lenn0nn0  12908  supxrun  12979  difelfzle  13298  elfzo0z  13357  fzofzim  13362  fzo1fzo0n0  13366  elfzodifsumelfzo  13381  elfznelfzo  13420  injresinj  13436  mulexp  13750  expadd  13753  expmul  13756  facdiv  13929  hashgt12el2  14066  hashimarni  14084  leisorel  14102  fi1uzind  14139  pfxfv  14323  swrdswrdlem  14345  pfxccat3  14375  reuccatpfxs1lem  14387  repswswrd  14425  cshf1  14451  2cshwcshw  14466  cshimadifsn  14470  relexpindlem  14702  pwdif  15508  dvdsaddre2b  15944  addmodlteqALT  15962  ltoddhalfle  15998  halfleoddlt  15999  coprmprod  16294  coprmproddvds  16296  cncongr1  16300  oddprmgt2  16332  prmfac1  16354  infpnlem1  16539  prmgaplem5  16684  prmgaplem6  16685  cshwshashlem1  16725  setsstruct  16805  iscatd2  17307  initoeu2lem2  17646  clatleglb  18151  dfgrp3e  18590  mulgaddcom  18642  mulginvcom  18643  symgfvne  18903  f1rhm0to0ALT  19900  lsmcv  20318  assamulgscm  21015  psrvscafval  21069  mat1scmat  21596  cramer0  21747  chpscmat  21899  fvmptnn04ifa  21907  fvmptnn04ifc  21909  fvmptnn04ifd  21910  fiinopn  21958  opnneissb  22173  cnpimaex  22315  regsep  22393  hausnei2  22412  cmpsublem  22458  cmpsub  22459  filufint  22979  blssps  23485  blss  23486  mblsplit  24601  bcmono  26330  gausslemma2dlem1a  26418  2sqlem10  26481  elntg2  27256  upgrex  27365  numedglnl  27417  ausgrumgri  27440  ausgrusgri  27441  usgredg2vtxeuALT  27492  ushgredgedg  27499  ushgredgedgloop  27501  edg0usgr  27523  0uhgrsubgr  27549  subumgredg2  27555  fusgrfisbase  27598  cusgrsizeinds  27722  cusgrsize2inds  27723  finsumvtxdg2size  27820  upgrewlkle2  27876  wlkl1loop  27907  pthdivtx  27998  2pthnloop  28000  upgrwlkdvde  28006  uhgrwkspthlem2  28023  usgr2pthlem  28032  usgr2pth  28033  clwlkl1loop  28052  crctcshwlkn0lem4  28079  wwlksnextproplem3  28177  wspn0  28190  umgr2adedgwlkonALT  28213  umgr2wlk  28215  umgr2wlkon  28216  elwwlks2  28232  clwwlkccatlem  28254  umgrclwwlkge2  28256  clwlkclwwlklem2  28265  clwlkclwwlkf1lem2  28270  clwlkclwwlkf  28273  clwwlknlbonbgr1  28304  clwwlkn1loopb  28308  clwwlkel  28311  clwwlkext2edg  28321  clwwlknonex2lem2  28373  clwwlknonex2  28374  clwwlknonex2e  28375  1pthon2v  28418  uhgr3cyclex  28447  eupth2lem3lem6  28498  frgr3vlem1  28538  3cyclfrgrrn1  28550  frgrnbnb  28558  frgrwopreglem4a  28575  2clwwlk2clwwlklem  28611  wlkl0  28632  frgrregord013  28660  frgrregord13  28661  frgrogt3nreg  28662  friendship  28664  chcompl  29505  spansncol  29831  hoaddsub  30079  bnj600  32799  sconnpht  33091  satffunlem  33263  satfvel  33274  msubvrs  33422  funpsstri  33645  imp5p  34427  cntotbnd  35881  clmgmOLD  35936  grpomndo  35960  rngoneglmul  36028  rngonegrmul  36029  zerdivemp1x  36032  atlex  37257  cvlexch1  37269  cvlsupr4  37286  cvlsupr5  37287  cvlsupr6  37288  2llnneN  37350  athgt  37397  llnle  37459  lplnle  37481  lvoli2  37522  pmaple  37702  dalawlem10  37821  dalawlem13  37824  dalawlem14  37825  dalaw  37827  lhp2lt  37942  ldilval  38054  cdleme50trn2  38492  cdlemf  38504  cdlemg18b  38620  tendotp  38702  tendospcanN  38964  dihmeetlem3N  39246  dvh4dimlem  39384  pell14qrexpclnn0  40604  pell1qrgap  40612  aomclem2  40796  rngunsnply  40914  relexpaddss  41215  rp-simp2  41290  gneispaceel2  41643  bi33imp12  41999  bi23imp13  42000  bi13imp23  42001  bi23imp1  42004  bi123imp0  42005  ee333  42016  jaoded  42075  e333  42242  suctrALTcf  42431  suctrALTcfVD  42432  ax6e2ndeqALT  42440  mullimc  43047  mullimcf  43054  f1oresf1o2  44670  fzopredsuc  44703  subsubelfzo0  44706  elsetpreimafvbi  44731  iccpartimp  44757  iccpartigtl  44763  lswn0  44784  poprelb  44864  fmtnofac1  44910  lighneallem2  44946  lighneallem3  44947  lighneallem4  44950  mogoldbblem  45060  fpprel2  45081  gbegt5  45101  sbgoldbaltlem1  45119  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  lidldomn1  45367  cznnring  45402  rngccatidALTV  45435  ringccatidALTV  45498  scmsuppss  45596  lmodvsmdi  45606  gsumlsscl  45607  lindslinindimp2lem1  45687  lindsrng01  45697  elfzolborelfzop1  45748  difmodm1lt  45756  fllog2  45802  dignn0flhalflem1  45849  rrxlinesc  45969  itschlc0yqe  45994  itsclc0xyqsol  46002  itscnhlinecirc02p  46019