Theorem 3imp 1117

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  3imp31  1118  3imp231  1119  3impb  1121  bi23imp13  1122  3impib  1123  3imp1  1355  3impd  1356  3jao  1434  biimp3ar  1479  3elpr2eq  4839  wefrc  5614  iotan0  6478  f1ssf1  6802  fveqdmss  7022  funelss  7991  poxp  8070  fvn0elsuppb  8123  suppfnss  8131  smo11  8297  odi  8508  omass  8509  nndi  8553  nnmass  8554  undifixp  8876  domunfican  9226  preleqg  9531  dfac8alem  9946  fin33i  10287  domtriomlem  10360  axdc3lem2  10369  axdc3lem4  10371  axdc4lem  10373  ttukeyg  10435  axdclem  10437  grupr  10716  nqereu  10848  squeeze0  12054  rpnnen1lem5  12926  xnn0lenn0nn0  13192  supxrun  13263  difelfzle  13590  elfzo0z  13651  fzofzim  13659  fzo1fzo0n0  13665  elfzodifsumelfzo  13681  elfznelfzo  13723  injresinj  13741  mulexp  14058  expadd  14061  expmul  14064  facdiv  14244  hashgt12el2  14380  hashimarni  14398  leisorel  14417  fi1uzind  14464  pfxfv  14640  swrdswrdlem  14661  pfxccat3  14691  reuccatpfxs1lem  14703  repswswrd  14741  cshf1  14767  2cshwcshw  14782  cshimadifsn  14786  relexpindlem  15020  pwdif  15828  dvdsaddre2b  16271  addmodlteqALT  16289  ltoddhalfle  16325  halfleoddlt  16326  coprmprod  16625  coprmproddvds  16627  cncongr1  16631  oddprmgt2  16664  prmfac1  16685  infpnlem1  16876  prmgaplem5  17021  prmgaplem6  17022  cshwshashlem1  17061  setsstruct  17141  iscatd2  17642  initoeu2lem2  17977  clatleglb  18479  dfgrp3e  19011  mulgaddcom  19069  mulginvcom  19070  symgfvne  19350  lsmcv  21137  assamulgscm  21879  psrvscafval  21926  mat1scmat  22525  cramer0  22676  chpscmat  22828  fvmptnn04ifa  22836  fvmptnn04ifc  22838  fvmptnn04ifd  22839  fiinopn  22887  opnneissb  23100  cnpimaex  23242  regsep  23320  hausnei2  23339  cmpsublem  23385  cmpsub  23386  filufint  23906  blssps  24410  blss  24411  mblsplit  25520  dvply2g  26272  taylply2  26354  bcmono  27261  gausslemma2dlem1a  27349  2sqlem10  27412  eqcuts3  27816  addsuniflem  28013  negsunif  28067  sltmuls2  28160  precsexlem11  28229  bdaypw2n0bndlem  28475  elreno2  28507  elntg2  29074  upgrex  29181  numedglnl  29233  ausgrumgri  29256  ausgrusgri  29257  usgredg2vtxeuALT  29311  ushgredgedg  29318  ushgredgedgloop  29320  edg0usgr  29342  0uhgrsubgr  29368  subumgredg2  29374  fusgrfisbase  29417  cusgrsizeinds  29541  cusgrsize2inds  29542  finsumvtxdg2size  29639  upgrewlkle2  29695  wlkl1loop  29726  pthdivtx  29815  2pthnloop  29819  upgrwlkdvde  29825  uhgrwkspthlem2  29842  usgr2pthlem  29851  usgr2pth  29852  clwlkl1loop  29871  crctcshwlkn0lem4  29901  wwlksnextproplem3  29999  wspn0  30012  umgr2adedgwlkonALT  30035  umgr2wlk  30037  umgr2wlkon  30038  elwwlks2  30057  clwwlkccatlem  30079  umgrclwwlkge2  30081  clwlkclwwlklem2  30090  clwlkclwwlkf1lem2  30095  clwlkclwwlkf  30098  clwwlknlbonbgr1  30129  clwwlkn1loopb  30133  clwwlkel  30136  clwwlkext2edg  30146  clwwlknonex2lem2  30198  clwwlknonex2  30199  clwwlknonex2e  30200  1pthon2v  30243  uhgr3cyclex  30272  eupth2lem3lem6  30323  frgr3vlem1  30363  3cyclfrgrrn1  30375  frgrnbnb  30383  frgrwopreglem4a  30400  2clwwlk2clwwlklem  30436  wlkl0  30457  frgrregord013  30485  frgrregord13  30486  frgrogt3nreg  30487  friendship  30489  chcompl  31333  spansncol  31659  hoaddsub  31907  bnj600  35114  sconnpht  35470  satffunlem  35642  satfvel  35653  msubvrs  35801  funpsstri  36007  imp5p  36552  cntotbnd  38176  clmgmOLD  38231  grpomndo  38255  rngoneglmul  38323  rngonegrmul  38324  zerdivemp1x  38327  qmapeldisjsim  39240  rnqmapeleldisjsim  39242  atlex  39821  cvlexch1  39833  cvlsupr4  39850  cvlsupr5  39851  cvlsupr6  39852  2llnneN  39914  athgt  39961  llnle  40023  lplnle  40045  lvoli2  40086  pmaple  40266  dalawlem10  40385  dalawlem13  40388  dalawlem14  40389  dalaw  40391  lhp2lt  40506  ldilval  40618  cdleme50trn2  41056  cdlemf  41068  cdlemg18b  41184  tendotp  41266  tendospcanN  41528  dihmeetlem3N  41810  dvh4dimlem  41948  pell14qrexpclnn0  43324  pell1qrgap  43332  aomclem2  43513  rngunsnply  43627  dflim5  43787  relexpaddss  44175  rp-simp2  44250  gneispaceel2  44601  bi33imp12  44948  bi13imp23  44949  bi23imp1  44952  bi123imp0  44953  ee333  44964  jaoded  45023  e333  45189  suctrALTcf  45378  suctrALTcfVD  45379  ax6e2ndeqALT  45387  mullimc  46073  mullimcf  46080  f1oresf1o2  47766  fzopredsuc  47799  subsubelfzo0  47802  nnmul2b  47806  2tceilhalfelfzo1  47811  2timesltsqm1  47854  muldvdsfacgt  47861  muldvdsfacm1  47862  elsetpreimafvbi  47878  iccpartimp  47904  iccpartigtl  47910  lswn0  47931  poprelb  48011  fmtnofac1  48060  lighneallem2  48096  lighneallem3  48097  lighneallem4  48100  nprmdvdsfacm1lem2  48111  mogoldbblem  48223  fpprel2  48244  gbegt5  48264  sbgoldbaltlem1  48282  bgoldbtbndlem2  48309  bgoldbtbndlem3  48310  clnbgrssedg  48344  grimuhgr  48390  uhgrimedgi  48393  uhgrimisgrgriclem  48433  uhgrimisgrgric  48434  clnbgrgrim  48437  grimedg  48438  grimgrtri  48452  usgrgrtrirex  48453  isubgr3stgrlem4  48472  grlimgrtri  48506  clnbgr3stgrgrlim  48522  gpgedgvtx1  48565  gpgvtxedg0  48566  gpgvtxedg1  48567  gpgcubic  48582  gpg5nbgr3star  48584  lidldomn1  48734  cznnring  48765  rngccatidALTV  48775  ringccatidALTV  48809  scmsuppss  48874  lmodvsmdi  48882  gsumlsscl  48883  lindslinindimp2lem1  48961  lindsrng01  48971  elfzolborelfzop1  49022  fllog2  49071  dignn0flhalflem1  49118  rrxlinesc  49238  itschlc0yqe  49263  itsclc0xyqsol  49271  itscnhlinecirc02p  49288