Theorem exp31 424

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
exp31	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	ex 417	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 417	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  exp41  439  exp42  440  imp5a  445  expl  462  anasss  471  an31s  666  exbiri  822  3exp  1137  exp516  1375  rexlimdva2  3168  r19.29af2  3273  reusv2lem2  5372  pwssun  5555  onmindif  6457  mpteqb  7011  dffo3f  7103  fompt  7115  fliftfun  7312  elovmpt3rab1  7672  ordsucss  7815  tfindsg  7858  tfrlem1  8363  tfrlem9  8373  oaordi  8532  oaordex  8544  oaass  8547  oarec  8548  omass  8566  oen0  8573  oeordsuc  8581  nnaordi  8605  omsmolem  8644  naddssim  8673  brinxper  8725  infensuc  9144  suppeqfsuppbi  9340  marypha1lem  9394  hartogs  9507  card2on  9517  tz9.12lem3  9762  infxpenlem  9998  cfcoflem  10257  isf32lem12  10349  zorn2lem6  10486  ondomon  10548  axrepnd  10580  fpwwe2lem11  10627  genpcd  10992  ltexprlem6  11027  axpre-sup  11155  negf1o  11645  recex  11847  uzaddcl  12929  nn01to3  12966  rpnnen1lem5  13006  xrsupsslem  13334  xrinfmsslem  13335  supxrunb1  13346  supxrunb2  13347  fz0fzelfz0  13664  fz0fzdiffz0  13667  elfzmlbp  13669  difelfzle  13671  fzo1fzo0n0  13746  elincfzoext  13754  ssfzo12bi  13792  elfznelfzo  13804  modaddmodup  13972  modfzo0difsn  13981  fsuppmapnn0fiubex  14030  seqf1o  14081  expcllem  14110  expeq0  14130  mulexp  14139  hashgt12el2  14462  hashimarni  14480  hash2prd  14514  fi1uzind  14546  swrdnd  14694  swrdswrdlem  14743  swrdswrd  14744  pfxccat3  14773  reuccatpfxs1  14786  repswswrd  14823  repswccat  14825  cshwidxmod  14842  2cshwcshw  14864  s4f1o  14957  wwlktovfo  14997  relexpindlem  15102  resqrex  15303  summo  15770  fsum2d  15824  modfsummods  15847  binom  15886  clim2prod  15944  fprod2d  16037  binomfallfac  16096  efexp  16158  demoivreALT  16258  divconjdvds  16374  addmodlteqALT  16384  dfgcd2  16605  lcmfunsnlem2lem1  16697  lcmfdvdsb  16702  lcmfun  16704  coprmprod  16720  coprmproddvdslem  16721  oddprmdvds  16964  ramcl  17090  prmgaplem6  17117  cshwsidrepswmod0  17155  cshwshashlem1  17156  cshwshashlem2  17157  ressress  17308  initoeu2lem1  18072  symggen  19541  pmtr3ncom  19546  gsumle  20216  srgmulgass  20300  srgbinom  20314  ringinvnzdiv  20385  rhmsubcrngclem2  20753  lmodvsmmulgdi  20999  nzerooringczr  21611  ofldchr  21707  psgndiflemB  21731  assamulgscmlem2  22031  mptcoe1fsupp  22356  coe1fzgsumdlem  22444  evl1gsumdlem  22497  scmatmulcl  22656  mdetdiagid  22738  pm2mpf1  22937  mptcoe1matfsupp  22940  mp2pm2mplem4  22947  chpdmat  22979  chfacfisf  22992  chfacfisfcpmat  22993  chcoeffeq  23024  topbas  23110  elcls  23211  elcls3  23221  2ndcdisj  23594  filufint  24058  ovoliunlem3  25644  dvge0  26146  ulmcn  26543  gausslemma2dlem3  27513  nosupbnd1  27859  nosupbnd2  27861  noinfbnd1  27874  noinfbnd2  27876  sizusglecusg  29794  upgriswlk  29971  2pthnloop  30061  crctcshwlkn0  30151  wlknwwlksnbij  30218  wwlksnred  30222  wwlksnext  30223  wwlksnextinj  30229  wwlksnextproplem2  30240  wwlksnextproplem3  30241  usgr2wspthons3  30297  clwwlkccatlem  30321  clwlkclwwlklem2a4  30329  clwlkclwwlklem2a  30330  clwlkclwwlklem2  30332  erclwwlktr  30354  clwwlkinwwlk  30372  clwwlkf  30379  clwwlkf1  30381  wwlksext2clwwlk  30389  clwwlknscsh  30394  umgr2cwwk2dif  30396  erclwwlkntr  30403  clwwlknonex2  30441  uhgr3cyclex  30514  upgr4cycl4dv4e  30517  eucrctshift  30575  3cyclfrgrrn1  30617  frgrwopreglem2  30645  frgrwopreglem5  30653  frgrwopreglem5ALT  30654  numclwwlk1lem2fo  30690  numclwlk2lem2f  30709  numclwlk2lem2f1o  30711  frgrreg  30726  friendshipgt3  30730  friendship  30731  ipasslem1  31164  shmodsi  31722  elspansn5  31907  h1datomi  31914  nmopsetretALT  32196  pjss2coi  32497  pj3cor1i  32542  mdexchi  32668  atcvat4i  32730  mdsymlem3  32738  mdsymlem4  32739  sumdmdii  32748  cdj3lem2b  32770  elabreximd  32837  iuninc  32886  iundisjf  32915  xrsmulgzz  33310  gsumvsca1  33527  gsumvsca2  33528  unitprodclb  33683  rprmdvdsprod  33805  1arithidom  33808  constrmon  34115  locfinreflem  34211  xrge0iifiso  34306  lmxrge0  34323  esumfzf  34440  sigaclfu2  34492  signstfvneq0  34940  satfrel  35840  satfrnmapom  35843  fmlafvel  35858  fmlasuc  35859  bccolsum  36212  faclimlem1  36216  segletr  36587  segleantisym  36588  outsideoftr  36602  exp5d  36795  elicc3  36809  finxpreclem2  38017  wl-sbcom2d  38197  poimirlem26  38278  mblfinlem3  38291  itg2addnc  38306  indexa  38365  disjlem19  39534  ax12indalem  39700  ax12inda2ALT  39701  cvrat4  40198  elpaddn0  40555  paddasslem5  40579  paddasslem14  40588  eldioph2  43476  pell1234qrdich  43571  oaabsb  44004  onmcl  44041  tfsconcat0b  44056  oaun3lem1  44084  oaun3lem2  44085  naddgeoa  44104  gneispb  44840  rexlimd3  45845  rexabslelem  46115  climsuselem1  46306  stoweidlem19  46716  stoweidlem20  46717  stoweidlem34  46731  wallispilem3  46764  sge0iunmpt  47115  meaiuninc3v  47181  smflimmpt  47507  or2expropbilem1  47752  fsetprcnexALT  47782  2reu8i  47833  2elfz2melfz  48038  subsubelfzo0  48047  iccpartigtl  48155  iccpartgt  48159  icceuelpartlem  48167  fargshiftf1  48173  ich2exprop  48203  ichreuopeq  48205  lighneallem3  48342  gbowgt5  48510  bgoldbtbndlem3  48555  bgoldbtbndlem4  48556  bgoldbtbnd  48557  tgblthelfgott  48563  grimco  48637  isuspgrimlem  48643  grimedg  48683  upgrwlkupwlk  48888  2zrngagrp  48997  lmodvsmdi  49142  ply1mulgsumlem1  49149  elfzolborelfzop1  49282  nnolog2flm1  49353  nn0sumshdiglemA  49382  eenglngeehlnmlem2  49501