Theorem exp31 419

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp41  434  exp42  435  imp5a  440  expl  457  anasss  466  an31s  653  exbiri  810  3exp  1119  exp516  1356  rexlimdva2  3163  r19.29af2  3273  reusv2lem2  5417  pwssun  5590  onmindif  6487  mpteqb  7048  dffo3f  7140  fompt  7152  fliftfun  7348  elovmpt3rab1  7710  ordsucss  7854  tfindsg  7898  tfrlem1  8432  tfrlem9  8441  oaordi  8602  oaordex  8614  oaass  8617  oarec  8618  omass  8636  oen0  8642  oeordsuc  8650  nnaordi  8674  omsmolem  8713  naddssim  8741  brinxper  8792  infensuc  9221  php3OLD  9287  suppeqfsuppbi  9448  marypha1lem  9502  hartogs  9613  card2on  9623  tz9.12lem3  9858  infxpenlem  10082  cfcoflem  10341  isf32lem12  10433  zorn2lem6  10570  ondomon  10632  axrepnd  10663  fpwwe2lem11  10710  genpcd  11075  ltexprlem6  11110  axpre-sup  11238  negf1o  11720  recex  11922  uzaddcl  12969  nn01to3  13006  rpnnen1lem5  13046  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  supxrunb2  13382  fz0fzelfz0  13691  fz0fzdiffz0  13694  elfzmlbp  13696  difelfzle  13698  fzo1fzo0n0  13767  elincfzoext  13774  ssfzo12bi  13811  elfznelfzo  13822  modaddmodup  13985  modfzo0difsn  13994  fsuppmapnn0fiubex  14043  seqf1o  14094  expcllem  14123  expeq0  14143  mulexp  14152  hashgt12el2  14472  hashimarni  14490  hash2prd  14524  fi1uzind  14556  swrdnd  14702  swrdswrdlem  14752  swrdswrd  14753  pfxccat3  14782  reuccatpfxs1  14795  repswswrd  14832  repswccat  14834  cshwidxmod  14851  2cshwcshw  14874  s4f1o  14967  wwlktovfo  15007  relexpindlem  15112  resqrex  15299  summo  15765  fsum2d  15819  modfsummods  15841  binom  15878  clim2prod  15936  fprod2d  16029  binomfallfac  16089  efexp  16149  demoivreALT  16249  divconjdvds  16363  addmodlteqALT  16373  dfgcd2  16593  lcmfunsnlem2lem1  16685  lcmfdvdsb  16690  lcmfun  16692  coprmprod  16708  coprmproddvdslem  16709  oddprmdvds  16950  ramcl  17076  prmgaplem6  17103  cshwsidrepswmod0  17142  cshwshashlem1  17143  cshwshashlem2  17144  ressress  17307  initoeu2lem1  18081  symggen  19512  pmtr3ncom  19517  srgmulgass  20244  srgbinom  20258  ringinvnzdiv  20324  rhmsubcrngclem2  20689  lmodvsmmulgdi  20917  nzerooringczr  21514  psgndiflemB  21641  assamulgscmlem2  21943  mptcoe1fsupp  22238  coe1fzgsumdlem  22328  evl1gsumdlem  22381  scmatmulcl  22545  mdetdiagid  22627  pm2mpf1  22826  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chpdmat  22868  chfacfisf  22881  chfacfisfcpmat  22882  chcoeffeq  22913  topbas  23000  elcls  23102  elcls3  23112  2ndcdisj  23485  filufint  23949  ovoliunlem3  25558  dvge0  26065  ulmcn  26460  gausslemma2dlem3  27430  nosupbnd1  27777  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2  27794  sizusglecusg  29499  upgriswlk  29677  2pthnloop  29767  crctcshwlkn0  29854  wlknwwlksnbij  29921  wwlksnred  29925  wwlksnext  29926  wwlksnextinj  29932  wwlksnextproplem2  29943  wwlksnextproplem3  29944  usgr2wspthons3  29997  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  erclwwlktr  30054  clwwlkinwwlk  30072  clwwlkf  30079  clwwlkf1  30081  wwlksext2clwwlk  30089  clwwlknscsh  30094  umgr2cwwk2dif  30096  erclwwlkntr  30103  clwwlknonex2  30141  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  eucrctshift  30275  3cyclfrgrrn1  30317  frgrwopreglem2  30345  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  numclwwlk1lem2fo  30390  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  frgrreg  30426  friendshipgt3  30430  friendship  30431  ipasslem1  30863  shmodsi  31421  elspansn5  31606  h1datomi  31613  nmopsetretALT  31895  pjss2coi  32196  pj3cor1i  32241  mdexchi  32367  atcvat4i  32429  mdsymlem3  32437  mdsymlem4  32438  sumdmdii  32447  cdj3lem2b  32469  elabreximd  32538  iuninc  32583  iundisjf  32611  xrsmulgzz  32992  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  ofldchr  33309  unitprodclb  33382  rprmdvdsprod  33527  1arithidom  33530  constrmon  33734  locfinreflem  33786  xrge0iifiso  33881  lmxrge0  33898  esumfzf  34033  sigaclfu2  34085  signstfvneq0  34549  satfrel  35335  satfrnmapom  35338  fmlafvel  35353  fmlasuc  35354  bccolsum  35701  faclimlem1  35705  segletr  36078  segleantisym  36079  outsideoftr  36093  exp5d  36268  elicc3  36283  finxpreclem2  37356  wl-sbcom2d  37515  poimirlem26  37606  mblfinlem3  37619  itg2addnc  37634  indexa  37693  disjlem19  38757  ax12indalem  38901  ax12inda2ALT  38902  cvrat4  39400  elpaddn0  39757  paddasslem5  39781  paddasslem14  39790  eldioph2  42718  pell1234qrdich  42817  oaabsb  43256  onmcl  43293  tfsconcat0b  43308  oaun3lem1  43336  oaun3lem2  43337  naddgeoa  43356  gneispb  44093  rexlimd3  45046  rexabslelem  45333  climsuselem1  45528  stoweidlem19  45940  stoweidlem20  45941  stoweidlem34  45955  wallispilem3  45988  sge0iunmpt  46339  meaiuninc3v  46405  smflimmpt  46731  or2expropbilem1  46947  fsetprcnexALT  46977  2reu8i  47028  2elfz2melfz  47233  subsubelfzo0  47241  iccpartigtl  47297  iccpartgt  47301  icceuelpartlem  47309  fargshiftf1  47315  ich2exprop  47345  ichreuopeq  47347  lighneallem3  47481  gbowgt5  47636  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgblthelfgott  47689  isuspgrimlem  47758  grimco  47764  grimedg  47787  upgrwlkupwlk  47863  2zrngagrp  47972  lmodvsmdi  48107  ply1mulgsumlem1  48115  elfzolborelfzop1  48248  nnolog2flm1  48324  nn0sumshdiglemA  48353  eenglngeehlnmlem2  48472