Theorem 3imp 1091

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  3imp31  1092  3imp231  1093  3impb  1095  3impib  1096  3imp1  1327  3impd  1328  3jao  1405  biimp3ar  1449  3elpr2eq  4711  wefrc  5401  predpo  6004  f1ssf1  6475  fveqdmss  6671  poxp  7627  fvn0elsuppb  7650  suppfnss  7658  smo11  7805  odi  8006  omass  8007  nndi  8050  nnmass  8051  undifixp  8295  domunfican  8586  preleqg  8872  pr2nelem  9224  dfac8alem  9249  fin33i  9589  domtriomlem  9662  axdc3lem2  9671  axdc3lem4  9673  axdc4lem  9675  ttukeyg  9737  axdclem  9739  grupr  10017  nqereu  10149  squeeze0  11344  rpnnen1lem5  12195  xnn0lenn0nn0  12454  supxrun  12525  difelfzle  12836  elfzo0z  12894  fzofzim  12899  fzo1fzo0n0  12903  elfzodifsumelfzo  12918  elfznelfzo  12957  injresinj  12973  mulexp  13283  expadd  13286  expmul  13289  facdiv  13462  hashgt12el2  13597  hashimarni  13615  leisorel  13631  fi1uzind  13666  2swrd1eqwrdeqOLD  13847  pfxfv  13864  swrdswrdlem  13886  pfxccat3  13936  swrdccat3OLD  13937  swrdccatidOLD  13948  reuccatpfxs1lem  13955  repswswrd  14003  cshf1  14034  2cshwcshw  14049  cshimadifsn  14053  relexpindlem  14283  pwdif  15083  dvdsaddre2b  15517  addmodlteqALT  15535  ltoddhalfle  15570  halfleoddlt  15571  coprmprod  15861  coprmproddvds  15863  cncongr1  15867  oddprmgt2  15899  prmfac1  15919  infpnlem1  16102  prmgaplem5  16247  prmgaplem6  16248  cshwshashlem1  16285  setsstruct  16379  iscatd2  16810  initoeu2lem2  17133  clatleglb  17594  dfgrp3e  17986  mulgaddcom  18035  mulginvcom  18036  symgfvne  18277  f1rhm0to0ALT  19217  lsmcv  19635  assamulgscm  19844  psrvscafval  19884  mat1scmat  20852  cramer0  21003  chpscmat  21154  fvmptnn04ifa  21162  fvmptnn04ifc  21164  fvmptnn04ifd  21165  fiinopn  21213  opnneissb  21426  cnpimaex  21568  regsep  21646  hausnei2  21665  cmpsublem  21711  cmpsub  21712  filufint  22232  blssps  22737  blss  22738  mblsplit  23836  bcmono  25555  gausslemma2dlem1a  25643  2sqlem10  25706  elntg2  26474  upgrex  26580  numedglnl  26632  ausgrumgri  26655  ausgrusgri  26656  usgredg2vtxeuALT  26707  ushgredgedg  26714  ushgredgedgloop  26716  edg0usgr  26738  0uhgrsubgr  26764  subumgredg2  26770  fusgrfisbase  26813  cusgrsizeinds  26937  cusgrsize2inds  26938  finsumvtxdg2size  27035  upgrewlkle2  27091  wlkl1loop  27122  pthdivtx  27218  2pthnloop  27220  upgrwlkdvde  27226  uhgrwkspthlem2  27243  usgr2pthlem  27252  usgr2pth  27253  clwlkl1loop  27272  crctcshwlkn0lem4  27299  wwlksnextproplem3  27413  wwlksnextproplem3OLD  27414  wspn0  27430  umgr2adedgwlkonALT  27453  umgr2wlk  27455  umgr2wlkon  27456  elwwlks2  27472  clwwlkccatlem  27495  umgrclwwlkge2  27497  clwlkclwwlklem2  27506  clwlkclwwlkf1lem2  27513  clwlkclwwlkf1lem2OLD  27514  clwlkclwwlkfOLD  27518  clwlkclwwlkf  27522  clwwlknlbonbgr1  27554  clwwlkn1loopb  27559  clwwlkel  27563  clwwlkext2edg  27579  clwwlknonex2lem2  27636  clwwlknonex2  27637  clwwlknonex2e  27638  1pthon2v  27682  uhgr3cyclex  27711  eupth2lem3lem6  27763  frgr3vlem1  27807  3cyclfrgrrn1  27819  frgrnbnb  27827  frgrwopreglem4a  27844  2clwwlk2clwwlklem  27883  wlkl0  27920  frgrregord013  27952  frgrregord13  27953  frgrogt3nreg  27954  friendship  27956  chcompl  28798  spansncol  29126  hoaddsub  29374  bnj600  31835  sconnpht  32058  msubvrs  32324  funpsstri  32525  imp5p  33177  cntotbnd  34513  clmgmOLD  34568  grpomndo  34592  rngoneglmul  34660  rngonegrmul  34661  zerdivemp1x  34664  atlex  35894  cvlexch1  35906  cvlsupr4  35923  cvlsupr5  35924  cvlsupr6  35925  2llnneN  35987  athgt  36034  llnle  36096  lplnle  36118  lvoli2  36159  pmaple  36339  dalawlem10  36458  dalawlem13  36461  dalawlem14  36462  dalaw  36464  lhp2lt  36579  ldilval  36691  cdleme50trn2  37129  cdlemf  37141  cdlemg18b  37257  tendotp  37339  tendospcanN  37601  dihmeetlem3N  37883  dvh4dimlem  38021  pell14qrexpclnn0  38856  pell1qrgap  38864  aomclem2  39048  rngunsnply  39166  relexpxpmin  39422  relexpaddss  39423  rp-simp2  39499  gneispaceel2  39854  bi33imp12  40240  bi23imp13  40241  bi13imp23  40242  bi23imp1  40245  bi123imp0  40246  ee333  40257  jaoded  40316  e333  40483  suctrALTcf  40672  suctrALTcfVD  40673  ax6e2ndeqALT  40681  mullimc  41326  mullimcf  41333  f1oresf1o2  42894  fzopredsuc  42927  subsubelfzo0  42930  iccpartimp  42947  iccpartigtl  42953  lswn0  42974  poprelb  43052  fmtnofac1  43098  lighneallem2  43137  lighneallem3  43138  lighneallem4  43141  mogoldbblem  43251  fpprel2  43272  gbegt5  43292  sbgoldbaltlem1  43310  bgoldbtbndlem2  43337  bgoldbtbndlem3  43338  lidldomn1  43554  cznnring  43589  rngccatidALTV  43622  ringccatidALTV  43685  scmsuppss  43784  lmodvsmdi  43794  gsumlsscl  43795  lindslinindimp2lem1  43878  lindsrng01  43888  elfzolborelfzop1  43940  difmodm1lt  43948  fllog2  43994  dignn0flhalflem1  44041  rrxlinesc  44088  itschlc0yqe  44113  itsclc0xyqsol  44121  itscnhlinecirc02p  44138