Theorem 3imp 1122

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

Syntax hints:   → wi 4   ∧ w3a 1097

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

This theorem is referenced by:  3imp31  1123  3imp231  1124  3impb  1126  bi23imp13  1127  3impib  1128  3imp1  1360  3impd  1361  3jao  1443  biimp3ar  1490  3elpr2eq  4863  wefrc  5639  iotan0  6507  f1ssf1  6835  fveqdmss  7055  funelss  8024  poxp  8103  fvn0elsuppb  8156  suppfnss  8164  smo11  8330  odi  8543  omass  8544  nndi  8588  nnmass  8589  undifixp  8912  domunfican  9262  preleqg  9567  dfac8alem  9982  fin33i  10323  domtriomlem  10396  axdc3lem2  10405  axdc3lem4  10407  axdc4lem  10409  ttukeyg  10471  axdclem  10473  grupr  10752  nqereu  10884  squeeze0  12092  rpnnen1lem5  12979  xnn0lenn0nn0  13245  supxrun  13316  difelfzle  13643  elfzo0z  13704  fzofzim  13712  fzo1fzo0n0  13718  elfzodifsumelfzo  13734  elfznelfzo  13776  injresinj  13794  mulexp  14111  expadd  14114  expmul  14117  facdiv  14297  hashgt12el2  14433  hashimarni  14451  leisorel  14470  fi1uzind  14517  pfxfv  14693  swrdswrdlem  14714  pfxccat3  14744  reuccatpfxs1lem  14756  repswswrd  14794  cshf1  14820  2cshwcshw  14835  cshimadifsn  14839  relexpindlem  15073  pwdif  15881  dvdsaddre2b  16324  addmodlteqALT  16342  ltoddhalfle  16378  halfleoddlt  16379  coprmprod  16678  coprmproddvds  16680  cncongr1  16684  oddprmgt2  16717  prmfac1  16738  infpnlem1  16929  prmgaplem5  17074  prmgaplem6  17075  cshwshashlem1  17114  setsstruct  17195  iscatd2  17696  initoeu2lem2  18031  clatleglb  18533  dfgrp3e  19065  mulgaddcom  19123  mulginvcom  19124  symgfvne  19404  lsmcv  21191  assamulgscm  21933  psrvscafval  21980  mat1scmat  22579  cramer0  22730  chpscmat  22882  fvmptnn04ifa  22890  fvmptnn04ifc  22892  fvmptnn04ifd  22893  fiinopn  22941  opnneissb  23154  cnpimaex  23296  regsep  23374  hausnei2  23393  cmpsublem  23439  cmpsub  23440  filufint  23960  blssps  24464  blss  24465  mblsplit  25574  dvply2g  26326  taylply2  26408  bcmono  27318  gausslemma2dlem1a  27406  2sqlem10  27469  eqcuts3  27874  addsuniflem  28071  negsunif  28125  sltmuls2  28218  precsexlem11  28287  bdaypw2n0bndlem  28533  elreno2  28565  elntg2  29132  upgrex  29239  numedglnl  29291  ausgrumgri  29314  ausgrusgri  29315  usgredg2vtxeuALT  29369  ushgredgedg  29376  ushgredgedgloop  29378  edg0usgr  29400  0uhgrsubgr  29426  subumgredg2  29432  fusgrfisbase  29475  cusgrsizeinds  29599  cusgrsize2inds  29600  finsumvtxdg2size  29697  upgrewlkle2  29753  wlkl1loop  29784  pthdivtx  29873  2pthnloop  29877  upgrwlkdvde  29883  uhgrwkspthlem2  29900  usgr2pthlem  29909  usgr2pth  29910  clwlkl1loop  29929  crctcshwlkn0lem4  29959  wwlksnextproplem3  30057  wspn0  30070  umgr2adedgwlkonALT  30093  umgr2wlk  30095  umgr2wlkon  30096  elwwlks2  30115  clwwlkccatlem  30137  umgrclwwlkge2  30139  clwlkclwwlklem2  30148  clwlkclwwlkf1lem2  30153  clwlkclwwlkf  30156  clwwlknlbonbgr1  30187  clwwlkn1loopb  30191  clwwlkel  30194  clwwlkext2edg  30204  clwwlknonex2lem2  30256  clwwlknonex2  30257  clwwlknonex2e  30258  1pthon2v  30301  uhgr3cyclex  30330  eupth2lem3lem6  30381  frgr3vlem1  30421  3cyclfrgrrn1  30433  frgrnbnb  30441  frgrwopreglem4a  30458  2clwwlk2clwwlklem  30494  wlkl0  30515  frgrregord013  30543  frgrregord13  30544  frgrogt3nreg  30545  friendship  30547  chcompl  31391  spansncol  31717  hoaddsub  31965  bnj600  35178  sconnpht  35543  satffunlem  35715  satfvel  35726  msubvrs  35874  funpsstri  36080  imp5p  36635  cntotbnd  38259  clmgmOLD  38314  grpomndo  38338  rngoneglmul  38406  rngonegrmul  38407  zerdivemp1x  38410  qmapeldisjsim  39323  rnqmapeleldisjsim  39325  atlex  39904  cvlexch1  39916  cvlsupr4  39933  cvlsupr5  39934  cvlsupr6  39935  2llnneN  39997  athgt  40044  llnle  40106  lplnle  40128  lvoli2  40169  pmaple  40349  dalawlem10  40468  dalawlem13  40471  dalawlem14  40472  dalaw  40474  lhp2lt  40589  ldilval  40701  cdleme50trn2  41139  cdlemf  41151  cdlemg18b  41267  tendotp  41349  tendospcanN  41611  dihmeetlem3N  41893  dvh4dimlem  42031  pell14qrexpclnn0  43407  pell1qrgap  43415  aomclem2  43596  rngunsnply  43710  dflim5  43870  relexpaddss  44258  rp-simp2  44333  gneispaceel2  44684  bi33imp12  45031  bi13imp23  45032  bi23imp1  45035  bi123imp0  45036  ee333  45047  jaoded  45106  e333  45272  suctrALTcf  45461  suctrALTcfVD  45462  ax6e2ndeqALT  45470  mullimc  46156  mullimcf  46163  f1oresf1o2  47849  fzopredsuc  47882  subsubelfzo0  47885  nnmul2b  47889  2tceilhalfelfzo1  47894  2timesltsqm1  47937  muldvdsfacgt  47944  muldvdsfacm1  47945  elsetpreimafvbi  47961  iccpartimp  47987  iccpartigtl  47993  lswn0  48014  poprelb  48094  fmtnofac1  48143  lighneallem2  48179  lighneallem3  48180  lighneallem4  48183  nprmdvdsfacm1lem2  48194  mogoldbblem  48306  fpprel2  48327  gbegt5  48347  sbgoldbaltlem1  48365  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  clnbgrssedg  48427  grimuhgr  48473  uhgrimedgi  48476  uhgrimisgrgriclem  48516  uhgrimisgrgric  48517  clnbgrgrim  48520  grimedg  48521  grimgrtri  48535  usgrgrtrirex  48536  isubgr3stgrlem4  48555  grlimgrtri  48589  clnbgr3stgrgrlim  48605  gpgedgvtx1  48648  gpgvtxedg0  48649  gpgvtxedg1  48650  gpgcubic  48665  gpg5nbgr3star  48667  lidldomn1  48817  cznnring  48848  rngccatidALTV  48858  ringccatidALTV  48892  scmsuppss  48957  lmodvsmdi  48965  gsumlsscl  48966  lindslinindimp2lem1  49044  lindsrng01  49054  elfzolborelfzop1  49105  fllog2  49154  dignn0flhalflem1  49201  rrxlinesc  49321  itschlc0yqe  49346  itsclc0xyqsol  49354  itscnhlinecirc02p  49371