Theorem 3imp 1249

Description: Importation inference. (Contributed by NM, 8-Apr-1994.)

Hypothesis

Ref	Expression
3imp.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
3imp	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 447	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 206	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3imp31  1250  3impa  1251  3impb  1252  3impia  1253  3impib  1254  3com23  1263  3imp21  1269  3imp3i2an  1270  3an1rs  1271  3imp1  1272  3impd  1273  syl3an2  1352  syl3an3  1353  3jao  1381  biimp3ar  1425  wefrc  5032  sotri2  5444  predpo  5615  fveqdmss  6262  poxp  7176  fvn0elsuppb  7199  smo11  7348  oawordri  7517  odi  7546  omass  7547  nndi  7590  nnmass  7591  undifixp  7830  isinf  8058  domunfican  8118  infssuni  8140  pr2nelem  8710  dfac8alem  8735  fin33i  9074  fin1a2lem10  9114  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  ttukeyg  9222  axdclem  9224  grupr  9498  nqereu  9630  squeeze0  10805  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  supxrun  12018  difelfzle  12321  elfzo0z  12377  fzofzim  12382  fzo1fzo0n0  12386  elfzodifsumelfzo  12401  elfznelfzo  12439  injresinj  12451  mulexp  12761  expadd  12764  expmul  12767  bernneq  12852  facdiv  12936  hashgt12el2  13071  hashimarni  13086  leisorel  13101  fi1uzind  13134  fi1uzindOLD  13140  2swrd1eqwrdeq  13306  swrdswrdlem  13311  swrdccat3  13343  swrdccatid  13348  repswswrd  13382  cshf1  13407  2cshwcshw  13422  cshimadifsn  13426  swrdco  13434  relexpindlem  13651  dvdsaddre2b  14867  addmodlteqALT  14885  ltoddhalfle  14923  halfleoddlt  14924  dfgcd2  15101  coprmprod  15213  coprmproddvds  15215  cncongr1  15219  oddprmgt2  15249  prmfac1  15269  infpnlem1  15452  prmgaplem5  15597  prmgaplem6  15598  cshwshashlem1  15640  iscatd2  16165  initoeu2lem2  16488  clatleglb  16949  dfgrp3e  17338  mulgaddcom  17387  mulginvcom  17388  symgfvne  17631  f1rhm0to0ALT  18564  lmodvsmmulgdi  18721  lsmcv  18962  assamulgscm  19171  psrvscafval  19211  mamufacex  20014  mat1scmat  20164  gsummatr01lem4  20283  cramer0  20315  chpscmat  20466  fvmptnn04ifa  20474  fvmptnn04ifc  20476  fvmptnn04ifd  20477  fiinopn  20531  opnneissb  20728  cnpimaex  20870  regsep  20948  hausnei2  20967  cmpsublem  21012  cmpsub  21013  filufint  21534  blssps  22039  blss  22040  mblsplit  23107  bcmono  24802  gausslemma2dlem1a  24890  2sqlem10  24953  upgrex  25759  usgraedg4  25916  usgrafisinds  25942  nbgraf1olem3  25972  cusgrasizeinds  26004  cusgrasize2inds  26005  1pthoncl  26122  2pthoncl  26133  wlkdvspthlem  26137  wlkdvspth  26138  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  usgra2wlkspth  26149  3v3e3cycl1  26172  constr3trl  26187  constr3pth  26188  constr3cycl  26189  4cycl4v4e  26194  4cycl4dv  26195  4cycl4dv4e  26196  wwlkm1edg  26263  wwlkextproplem3  26271  clwlkisclwwlklem1  26315  clwwlkel  26321  clwwlkext2edg  26330  usg2cwwk2dif  26348  clwlkf1clwwlklem  26376  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  el2wlkonotot0  26399  usg2wlkonot  26410  usg2wotspth  26411  cusgraiffrusgra  26467  rusgrasn  26472  eupatrl  26495  frgraunss  26522  3cyclfrgrarn1  26539  frgranbnb  26547  vdfrgra0  26549  usgn0fidegnn0  26556  frgrawopreglem2  26572  frgrawopreglem5  26575  clwwlkextfrlem1  26603  numclwwlkovf2ex  26613  extwwlkfab  26617  numclwlk1lem2foa  26618  frgraregord013  26645  frgraregord13  26646  frgraogt3nreg  26647  friendship  26649  chcompl  27483  spansncol  27811  hoaddsub  28059  bnj600  30243  sconpht  30465  msubvrs  30711  funpsstri  30909  imp5p  31475  cntotbnd  32765  clmgmOLD  32820  grpomndo  32844  rngoneglmul  32912  rngonegrmul  32913  zerdivemp1x  32916  atlex  33621  cvlexch1  33633  cvlsupr4  33650  cvlsupr5  33651  cvlsupr6  33652  2llnneN  33713  athgt  33760  llnle  33822  lplnle  33844  lvoli2  33885  pmaple  34065  dalawlem10  34184  dalawlem13  34187  dalawlem14  34188  dalaw  34190  lhp2lt  34305  ldilval  34417  cdleme50trn2  34857  cdlemf  34869  cdlemg18b  34985  tendotp  35067  tendospcanN  35330  dihmeetlem3N  35612  dvh4dimlem  35750  pell14qrexpclnn0  36448  pell1qrgap  36456  aomclem2  36643  rngunsnply  36762  relexpxpmin  37028  relexpaddss  37029  rp-simp2  37107  gneispaceel2  37462  bi33imp12  37717  bi23imp13  37718  bi13imp23  37719  bi23imp1  37722  bi123imp0  37723  ee333  37734  jaoded  37803  eel12131  37959  e333  37981  3imp231  38066  suctrALTcf  38180  suctrALTcfVD  38181  ax6e2ndeqALT  38189  mullimc  38683  mullimcf  38690  fzopredsuc  39946  iccpartimp  39955  iccpartigtl  39961  fmtnofac1  40020  pwdif  40039  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  gbegt5  40183  sgoldbaltlem1  40201  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  lswn0  40242  pfxfv  40262  pfxccat3  40289  reuccatpfxs1lem  40296  f1ssf1  40328  subsubelfzo0  40359  uhgrauhgrbi  40377  ausgrumgri  40397  ausgrusgri  40398  usgredg2vtxeuALT  40449  ushgredgedga  40456  ushgredgedgaloop  40458  edg0usgr  40479  0uhgrsubgr  40503  subumgredg2  40509  fusgrfisbase  40547  cusgrsizeinds  40668  cusgrsize2inds  40669  upgrewlkle2  40808  1wlkl1loop  40842  pthdivtx  40935  2pthnloop  40937  upgrwlkdvde  40943  uhgr1wlkspthlem2  40960  usgr2pthlem  40969  usgr2pth  40970  clwlkl1loop  40989  cyclnsPth  41006  crctcsh1wlkn0lem4  41016  wwlksnextproplem3  41117  umgr2adedgwlkonALT  41154  umgr2wlk  41156  umgr2wlkon  41157  elwwlks2  41170  clwlkclwwlklem2  41209  umgrclwwlksge2  41219  clwwlksel  41221  clwwlksext2edg  41230  clwwnisshclwwsn  41237  1pthon2v-av  41320  uhgr3cyclex  41349  eupth2lem3lem6  41401  frgr3vlem1  41443  3cyclfrgrrn1  41455  frgrnbnb  41463  frgrwopreglem5  41485  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  av-numclwlk1lem2foa  41521  av-frgraregord013  41549  av-frgraregord13  41550  av-frgraogt3nreg  41551  av-friendship  41553  lidldomn1  41711  cznnring  41748  rngccatidALTV  41781  ringccatidALTV  41844  scmsuppss  41947  lmodvsmdi  41957  gsumlsscl  41958  lindslinindimp2lem1  42041  lindsrng01  42051  elfzolborelfzop1  42103  difmodm1lt  42111  fllog2  42160  dignn0flhalflem1  42207