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  4830  wefrc  5543  predpo  6160  iotan0  6339  f1ssf1  6640  fveqdmss  6840  funelss  7740  poxp  7816  fvn0elsuppb  7841  suppfnss  7849  smo11  7995  odi  8199  omass  8200  nndi  8243  nnmass  8244  undifixp  8492  domunfican  8785  preleqg  9072  pr2nelem  9424  dfac8alem  9449  fin33i  9785  domtriomlem  9858  axdc3lem2  9867  axdc3lem4  9869  axdc4lem  9871  ttukeyg  9933  axdclem  9935  grupr  10213  nqereu  10345  squeeze0  11537  rpnnen1lem5  12374  xnn0lenn0nn0  12632  supxrun  12703  difelfzle  13014  elfzo0z  13073  fzofzim  13078  fzo1fzo0n0  13082  elfzodifsumelfzo  13097  elfznelfzo  13136  injresinj  13152  mulexp  13462  expadd  13465  expmul  13468  facdiv  13641  hashgt12el2  13778  hashimarni  13796  leisorel  13812  fi1uzind  13849  pfxfv  14038  swrdswrdlem  14060  pfxccat3  14090  reuccatpfxs1lem  14102  repswswrd  14140  cshf1  14166  2cshwcshw  14181  cshimadifsn  14185  relexpindlem  14416  pwdif  15217  dvdsaddre2b  15651  addmodlteqALT  15669  ltoddhalfle  15704  halfleoddlt  15705  coprmprod  15999  coprmproddvds  16001  cncongr1  16005  oddprmgt2  16037  prmfac1  16057  infpnlem1  16240  prmgaplem5  16385  prmgaplem6  16386  cshwshashlem1  16423  setsstruct  16517  iscatd2  16946  initoeu2lem2  17269  clatleglb  17730  dfgrp3e  18193  mulgaddcom  18245  mulginvcom  18246  symgfvne  18503  f1rhm0to0ALT  19488  lsmcv  19907  assamulgscm  20124  psrvscafval  20164  mat1scmat  21142  cramer0  21293  chpscmat  21444  fvmptnn04ifa  21452  fvmptnn04ifc  21454  fvmptnn04ifd  21455  fiinopn  21503  opnneissb  21716  cnpimaex  21858  regsep  21936  hausnei2  21955  cmpsublem  22001  cmpsub  22002  filufint  22522  blssps  23028  blss  23029  mblsplit  24127  bcmono  25847  gausslemma2dlem1a  25935  2sqlem10  25998  elntg2  26765  upgrex  26871  numedglnl  26923  ausgrumgri  26946  ausgrusgri  26947  usgredg2vtxeuALT  26998  ushgredgedg  27005  ushgredgedgloop  27007  edg0usgr  27029  0uhgrsubgr  27055  subumgredg2  27061  fusgrfisbase  27104  cusgrsizeinds  27228  cusgrsize2inds  27229  finsumvtxdg2size  27326  upgrewlkle2  27382  wlkl1loop  27413  pthdivtx  27504  2pthnloop  27506  upgrwlkdvde  27512  uhgrwkspthlem2  27529  usgr2pthlem  27538  usgr2pth  27539  clwlkl1loop  27558  crctcshwlkn0lem4  27585  wwlksnextproplem3  27684  wspn0  27697  umgr2adedgwlkonALT  27720  umgr2wlk  27722  umgr2wlkon  27723  elwwlks2  27739  clwwlkccatlem  27761  umgrclwwlkge2  27763  clwlkclwwlklem2  27772  clwlkclwwlkf1lem2  27777  clwlkclwwlkf  27780  clwwlknlbonbgr1  27811  clwwlkn1loopb  27815  clwwlkel  27819  clwwlkext2edg  27829  clwwlknonex2lem2  27881  clwwlknonex2  27882  clwwlknonex2e  27883  1pthon2v  27926  uhgr3cyclex  27955  eupth2lem3lem6  28006  frgr3vlem1  28046  3cyclfrgrrn1  28058  frgrnbnb  28066  frgrwopreglem4a  28083  2clwwlk2clwwlklem  28119  wlkl0  28140  frgrregord013  28168  frgrregord13  28169  frgrogt3nreg  28170  friendship  28172  chcompl  29013  spansncol  29339  hoaddsub  29587  bnj600  32186  sconnpht  32471  satffunlem  32643  satfvel  32654  msubvrs  32802  funpsstri  33003  imp5p  33654  cntotbnd  35068  clmgmOLD  35123  grpomndo  35147  rngoneglmul  35215  rngonegrmul  35216  zerdivemp1x  35219  atlex  36446  cvlexch1  36458  cvlsupr4  36475  cvlsupr5  36476  cvlsupr6  36477  2llnneN  36539  athgt  36586  llnle  36648  lplnle  36670  lvoli2  36711  pmaple  36891  dalawlem10  37010  dalawlem13  37013  dalawlem14  37014  dalaw  37016  lhp2lt  37131  ldilval  37243  cdleme50trn2  37681  cdlemf  37693  cdlemg18b  37809  tendotp  37891  tendospcanN  38153  dihmeetlem3N  38435  dvh4dimlem  38573  pell14qrexpclnn0  39456  pell1qrgap  39464  aomclem2  39648  rngunsnply  39766  relexpaddss  40056  rp-simp2  40132  gneispaceel2  40487  bi33imp12  40817  bi23imp13  40818  bi13imp23  40819  bi23imp1  40822  bi123imp0  40823  ee333  40834  jaoded  40893  e333  41060  suctrALTcf  41249  suctrALTcfVD  41250  ax6e2ndeqALT  41258  mullimc  41890  mullimcf  41897  f1oresf1o2  43484  fzopredsuc  43517  subsubelfzo0  43520  elsetpreimafvbi  43545  iccpartimp  43571  iccpartigtl  43577  lswn0  43598  poprelb  43680  fmtnofac1  43726  lighneallem2  43765  lighneallem3  43766  lighneallem4  43769  mogoldbblem  43879  fpprel2  43900  gbegt5  43920  sbgoldbaltlem1  43938  bgoldbtbndlem2  43965  bgoldbtbndlem3  43966  lidldomn1  44186  cznnring  44221  rngccatidALTV  44254  ringccatidALTV  44317  scmsuppss  44414  lmodvsmdi  44424  gsumlsscl  44425  lindslinindimp2lem1  44507  lindsrng01  44517  elfzolborelfzop1  44568  difmodm1lt  44576  fllog2  44622  dignn0flhalflem1  44669  rrxlinesc  44716  itschlc0yqe  44741  itsclc0xyqsol  44749  itscnhlinecirc02p  44766