Theorem 3imp 1111

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3imp31  1112  3imp231  1113  3impb  1115  3impib  1116  3imp1  1347  3impd  1348  3jao  1425  biimp3ar  1470  3elpr2eq  4930  wefrc  5694  iotan0  6563  f1ssf1  6894  fveqdmss  7112  funelss  8088  poxp  8169  fvn0elsuppb  8222  suppfnss  8230  smo11  8420  odi  8635  omass  8636  nndi  8679  nnmass  8680  undifixp  8992  domunfican  9389  preleqg  9684  pr2nelemOLD  10072  dfac8alem  10098  fin33i  10438  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  ttukeyg  10586  axdclem  10588  grupr  10866  nqereu  10998  squeeze0  12198  rpnnen1lem5  13046  xnn0lenn0nn0  13307  supxrun  13378  difelfzle  13698  elfzo0z  13758  fzofzim  13763  fzo1fzo0n0  13767  elfzodifsumelfzo  13782  elfznelfzo  13822  injresinj  13838  mulexp  14152  expadd  14155  expmul  14158  facdiv  14336  hashgt12el2  14472  hashimarni  14490  leisorel  14509  fi1uzind  14556  pfxfv  14730  swrdswrdlem  14752  pfxccat3  14782  reuccatpfxs1lem  14794  repswswrd  14832  cshf1  14858  2cshwcshw  14874  cshimadifsn  14878  relexpindlem  15112  pwdif  15916  dvdsaddre2b  16355  addmodlteqALT  16373  ltoddhalfle  16409  halfleoddlt  16410  coprmprod  16708  coprmproddvds  16710  cncongr1  16714  oddprmgt2  16746  prmfac1  16767  infpnlem1  16957  prmgaplem5  17102  prmgaplem6  17103  cshwshashlem1  17143  setsstruct  17223  iscatd2  17739  initoeu2lem2  18082  clatleglb  18588  dfgrp3e  19080  mulgaddcom  19138  mulginvcom  19139  symgfvne  19422  lsmcv  21166  assamulgscm  21944  psrvscafval  21991  mat1scmat  22566  cramer0  22717  chpscmat  22869  fvmptnn04ifa  22877  fvmptnn04ifc  22879  fvmptnn04ifd  22880  fiinopn  22928  opnneissb  23143  cnpimaex  23285  regsep  23363  hausnei2  23382  cmpsublem  23428  cmpsub  23429  filufint  23949  blssps  24455  blss  24456  mblsplit  25586  dvply2g  26344  taylply2  26427  bcmono  27339  gausslemma2dlem1a  27427  2sqlem10  27490  addsuniflem  28052  negsunif  28105  ssltmul2  28192  precsexlem11  28259  elntg2  29018  upgrex  29127  numedglnl  29179  ausgrumgri  29202  ausgrusgri  29203  usgredg2vtxeuALT  29257  ushgredgedg  29264  ushgredgedgloop  29266  edg0usgr  29288  0uhgrsubgr  29314  subumgredg2  29320  fusgrfisbase  29363  cusgrsizeinds  29488  cusgrsize2inds  29489  finsumvtxdg2size  29586  upgrewlkle2  29642  wlkl1loop  29674  pthdivtx  29765  2pthnloop  29767  upgrwlkdvde  29773  uhgrwkspthlem2  29790  usgr2pthlem  29799  usgr2pth  29800  clwlkl1loop  29819  crctcshwlkn0lem4  29846  wwlksnextproplem3  29944  wspn0  29957  umgr2adedgwlkonALT  29980  umgr2wlk  29982  umgr2wlkon  29983  elwwlks2  29999  clwwlkccatlem  30021  umgrclwwlkge2  30023  clwlkclwwlklem2  30032  clwlkclwwlkf1lem2  30037  clwlkclwwlkf  30040  clwwlknlbonbgr1  30071  clwwlkn1loopb  30075  clwwlkel  30078  clwwlkext2edg  30088  clwwlknonex2lem2  30140  clwwlknonex2  30141  clwwlknonex2e  30142  1pthon2v  30185  uhgr3cyclex  30214  eupth2lem3lem6  30265  frgr3vlem1  30305  3cyclfrgrrn1  30317  frgrnbnb  30325  frgrwopreglem4a  30342  2clwwlk2clwwlklem  30378  wlkl0  30399  frgrregord013  30427  frgrregord13  30428  frgrogt3nreg  30429  friendship  30431  chcompl  31274  spansncol  31600  hoaddsub  31848  bnj600  34895  sconnpht  35197  satffunlem  35369  satfvel  35380  msubvrs  35528  funpsstri  35729  imp5p  36277  cntotbnd  37756  clmgmOLD  37811  grpomndo  37835  rngoneglmul  37903  rngonegrmul  37904  zerdivemp1x  37907  atlex  39272  cvlexch1  39284  cvlsupr4  39301  cvlsupr5  39302  cvlsupr6  39303  2llnneN  39366  athgt  39413  llnle  39475  lplnle  39497  lvoli2  39538  pmaple  39718  dalawlem10  39837  dalawlem13  39840  dalawlem14  39841  dalaw  39843  lhp2lt  39958  ldilval  40070  cdleme50trn2  40508  cdlemf  40520  cdlemg18b  40636  tendotp  40718  tendospcanN  40980  dihmeetlem3N  41262  dvh4dimlem  41400  pell14qrexpclnn0  42822  pell1qrgap  42830  aomclem2  43012  rngunsnply  43130  dflim5  43291  relexpaddss  43680  rp-simp2  43755  gneispaceel2  44106  bi33imp12  44461  bi23imp13  44462  bi13imp23  44463  bi23imp1  44466  bi123imp0  44467  ee333  44478  jaoded  44537  e333  44704  suctrALTcf  44893  suctrALTcfVD  44894  ax6e2ndeqALT  44902  mullimc  45537  mullimcf  45544  f1oresf1o2  47206  fzopredsuc  47238  subsubelfzo0  47241  elsetpreimafvbi  47265  iccpartimp  47291  iccpartigtl  47297  lswn0  47318  poprelb  47398  fmtnofac1  47444  lighneallem2  47480  lighneallem3  47481  lighneallem4  47484  mogoldbblem  47594  fpprel2  47615  gbegt5  47635  sbgoldbaltlem1  47653  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  clnbgrssedg  47713  grimuhgr  47762  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrim  47786  grimedg  47787  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  lidldomn1  47954  cznnring  47985  rngccatidALTV  47995  ringccatidALTV  48029  scmsuppss  48097  lmodvsmdi  48107  gsumlsscl  48108  lindslinindimp2lem1  48187  lindsrng01  48197  elfzolborelfzop1  48248  difmodm1lt  48256  fllog2  48302  dignn0flhalflem1  48349  rrxlinesc  48469  itschlc0yqe  48494  itsclc0xyqsol  48502  itscnhlinecirc02p  48519