Theorem 3imp 1113

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  3imp31  1114  3imp231  1115  3impb  1117  3impib  1118  3imp1  1349  3impd  1350  3jao  1427  biimp3ar  1472  3elpr2eq  4804  wefrc  5530  predpo  6158  iotan0  6348  f1ssf1  6670  fveqdmss  6877  funelss  7796  poxp  7873  fvn0elsuppb  7901  suppfnss  7909  smo11  8079  odi  8285  omass  8286  nndi  8329  nnmass  8330  undifixp  8593  domunfican  8922  preleqg  9208  pr2nelem  9583  dfac8alem  9608  fin33i  9948  domtriomlem  10021  axdc3lem2  10030  axdc3lem4  10032  axdc4lem  10034  ttukeyg  10096  axdclem  10098  grupr  10376  nqereu  10508  squeeze0  11700  rpnnen1lem5  12542  xnn0lenn0nn0  12800  supxrun  12871  difelfzle  13190  elfzo0z  13249  fzofzim  13254  fzo1fzo0n0  13258  elfzodifsumelfzo  13273  elfznelfzo  13312  injresinj  13328  mulexp  13639  expadd  13642  expmul  13645  facdiv  13818  hashgt12el2  13955  hashimarni  13973  leisorel  13991  fi1uzind  14028  pfxfv  14212  swrdswrdlem  14234  pfxccat3  14264  reuccatpfxs1lem  14276  repswswrd  14314  cshf1  14340  2cshwcshw  14355  cshimadifsn  14359  relexpindlem  14591  pwdif  15395  dvdsaddre2b  15831  addmodlteqALT  15849  ltoddhalfle  15885  halfleoddlt  15886  coprmprod  16181  coprmproddvds  16183  cncongr1  16187  oddprmgt2  16219  prmfac1  16241  infpnlem1  16426  prmgaplem5  16571  prmgaplem6  16572  cshwshashlem1  16612  setsstruct  16705  iscatd2  17138  initoeu2lem2  17475  clatleglb  17978  dfgrp3e  18417  mulgaddcom  18469  mulginvcom  18470  symgfvne  18727  f1rhm0to0ALT  19715  lsmcv  20132  assamulgscm  20815  psrvscafval  20869  mat1scmat  21390  cramer0  21541  chpscmat  21693  fvmptnn04ifa  21701  fvmptnn04ifc  21703  fvmptnn04ifd  21704  fiinopn  21752  opnneissb  21965  cnpimaex  22107  regsep  22185  hausnei2  22204  cmpsublem  22250  cmpsub  22251  filufint  22771  blssps  23276  blss  23277  mblsplit  24383  bcmono  26112  gausslemma2dlem1a  26200  2sqlem10  26263  elntg2  27030  upgrex  27137  numedglnl  27189  ausgrumgri  27212  ausgrusgri  27213  usgredg2vtxeuALT  27264  ushgredgedg  27271  ushgredgedgloop  27273  edg0usgr  27295  0uhgrsubgr  27321  subumgredg2  27327  fusgrfisbase  27370  cusgrsizeinds  27494  cusgrsize2inds  27495  finsumvtxdg2size  27592  upgrewlkle2  27648  wlkl1loop  27679  pthdivtx  27770  2pthnloop  27772  upgrwlkdvde  27778  uhgrwkspthlem2  27795  usgr2pthlem  27804  usgr2pth  27805  clwlkl1loop  27824  crctcshwlkn0lem4  27851  wwlksnextproplem3  27949  wspn0  27962  umgr2adedgwlkonALT  27985  umgr2wlk  27987  umgr2wlkon  27988  elwwlks2  28004  clwwlkccatlem  28026  umgrclwwlkge2  28028  clwlkclwwlklem2  28037  clwlkclwwlkf1lem2  28042  clwlkclwwlkf  28045  clwwlknlbonbgr1  28076  clwwlkn1loopb  28080  clwwlkel  28083  clwwlkext2edg  28093  clwwlknonex2lem2  28145  clwwlknonex2  28146  clwwlknonex2e  28147  1pthon2v  28190  uhgr3cyclex  28219  eupth2lem3lem6  28270  frgr3vlem1  28310  3cyclfrgrrn1  28322  frgrnbnb  28330  frgrwopreglem4a  28347  2clwwlk2clwwlklem  28383  wlkl0  28404  frgrregord013  28432  frgrregord13  28433  frgrogt3nreg  28434  friendship  28436  chcompl  29277  spansncol  29603  hoaddsub  29851  bnj600  32566  sconnpht  32858  satffunlem  33030  satfvel  33041  msubvrs  33189  funpsstri  33409  imp5p  34186  cntotbnd  35640  clmgmOLD  35695  grpomndo  35719  rngoneglmul  35787  rngonegrmul  35788  zerdivemp1x  35791  atlex  37016  cvlexch1  37028  cvlsupr4  37045  cvlsupr5  37046  cvlsupr6  37047  2llnneN  37109  athgt  37156  llnle  37218  lplnle  37240  lvoli2  37281  pmaple  37461  dalawlem10  37580  dalawlem13  37583  dalawlem14  37584  dalaw  37586  lhp2lt  37701  ldilval  37813  cdleme50trn2  38251  cdlemf  38263  cdlemg18b  38379  tendotp  38461  tendospcanN  38723  dihmeetlem3N  39005  dvh4dimlem  39143  pell14qrexpclnn0  40332  pell1qrgap  40340  aomclem2  40524  rngunsnply  40642  relexpaddss  40944  rp-simp2  41019  gneispaceel2  41372  bi33imp12  41724  bi23imp13  41725  bi13imp23  41726  bi23imp1  41729  bi123imp0  41730  ee333  41741  jaoded  41800  e333  41967  suctrALTcf  42156  suctrALTcfVD  42157  ax6e2ndeqALT  42165  mullimc  42775  mullimcf  42782  f1oresf1o2  44398  fzopredsuc  44431  subsubelfzo0  44434  elsetpreimafvbi  44459  iccpartimp  44485  iccpartigtl  44491  lswn0  44512  poprelb  44592  fmtnofac1  44638  lighneallem2  44674  lighneallem3  44675  lighneallem4  44678  mogoldbblem  44788  fpprel2  44809  gbegt5  44829  sbgoldbaltlem1  44847  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  lidldomn1  45095  cznnring  45130  rngccatidALTV  45163  ringccatidALTV  45226  scmsuppss  45324  lmodvsmdi  45334  gsumlsscl  45335  lindslinindimp2lem1  45415  lindsrng01  45425  elfzolborelfzop1  45476  difmodm1lt  45484  fllog2  45530  dignn0flhalflem1  45577  rrxlinesc  45697  itschlc0yqe  45722  itsclc0xyqsol  45730  itscnhlinecirc02p  45747