Theorem exp31 425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp41  440  exp42  441  imp5a  446  expl  463  anasss  472  an31s  667  exbiri  823  3exp  1137  exp516  1375  rexlimdva2  3166  r19.29af2  3271  reusv2lem2  5361  pwssun  5543  onmindif  6450  mpteqb  7005  dffo3f  7098  fompt  7110  fliftfun  7312  elovmpt3rab1  7673  ordsucss  7818  tfindsg  7861  tfrlem1  8367  tfrlem9  8377  oaordi  8538  oaordex  8550  oaass  8553  oarec  8554  omass  8572  oen0  8579  oeordsuc  8587  nnaordi  8611  omsmolem  8650  naddssim  8679  brinxper  8731  infensuc  9158  suppeqfsuppbi  9355  marypha1lem  9409  hartogs  9522  card2on  9532  tz9.12lem3  9779  infxpenlem  10073  cfcoflem  10331  isf32lem12  10423  zorn2lem6  10560  ondomon  10628  axrepnd  10660  fpwwe2lem11  10707  genpcd  11072  ltexprlem6  11107  axpre-sup  11235  negf1o  11727  recex  11929  uzaddcl  13012  nn01to3  13049  rpnnen1lem5  13090  xrsupsslem  13418  xrinfmsslem  13419  supxrunb1  13430  supxrunb2  13431  fz0fzelfz0  13748  fz0fzdiffz0  13751  elfzmlbp  13753  difelfzle  13755  fzo1fzo0n0  13830  elincfzoext  13838  ssfzo12bi  13876  elfznelfzo  13888  modaddmodup  14057  modfzo0difsn  14066  fsuppmapnn0fiubex  14115  seqf1o  14166  expcllem  14195  expeq0  14215  mulexp  14224  hashgt12el2  14548  hashimarni  14566  hash2prd  14600  fi1uzind  14632  swrdnd  14784  swrdswrdlem  14833  swrdswrd  14834  pfxccat3  14863  reuccatpfxs1  14876  repswswrd  14915  repswccat  14917  cshwidxmod  14934  2cshwcshw  14956  s4f1o  15049  wwlktovfo  15091  relexpindlem  15196  resqrex  15397  summo  15863  fsum2d  15917  modfsummods  15940  binom  15979  clim2prod  16037  fprod2d  16128  binomfallfac  16187  efexp  16249  demoivreALT  16349  divconjdvds  16465  addmodlteqALT  16475  dfgcd2  16699  lcmfunsnlem2lem1  16793  lcmfdvdsb  16798  lcmfun  16800  coprmprod  16816  coprmproddvdslem  16817  oddprmdvds  17061  ramcl  17187  prmgaplem6  17214  cshwsidrepswmod0  17252  cshwshashlem1  17253  cshwshashlem2  17254  ressress  17405  initoeu2lem1  18169  mgmn0plusgplusf  18808  symggen  19664  pmtr3ncom  19669  gsumle  20339  srgmulgass  20423  srgbinom  20437  ringinvnzdiv  20512  rhmsubcrngclem2  20899  lmodvsmmulgdi  21152  nzerooringczr  21766  ofldchr  21862  psgndiflemB  21886  assamulgscmlem2  22188  mptcoe1fsupp  22513  coe1fzgsumdlem  22601  evl1gsumdlem  22654  scmatmulcl  22813  mdetdiagid  22895  pm2mpf1  23097  mptcoe1matfsupp  23100  mp2pm2mplem4  23107  chpdmat  23139  chfacfisf  23152  chfacfisfcpmat  23153  chcoeffeq  23184  topbas  23270  elcls  23371  elcls3  23381  2ndcdisj  23755  filufint  24219  ovoliunlem3  25805  dvge0  26306  ulmcn  26708  gausslemma2dlem3  27677  nosupbnd1  28053  nosupbnd2  28055  noinfbnd1  28068  noinfbnd2  28070  sizusglecusg  30026  upgriswlk  30203  2pthnloop  30299  crctcshwlkn0  30392  wlknwwlksnbij  30459  wwlksnred  30463  wwlksnext  30464  wwlksnextinj  30470  wwlksnextproplem2  30481  wwlksnextproplem3  30482  usgr2wspthons3  30538  clwwlkccatlem  30562  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  erclwwlktr  30595  clwwlkinwwlk  30613  clwwlkf  30620  clwwlkf1  30622  wwlksext2clwwlk  30630  clwwlknscsh  30635  umgr2cwwk2dif  30637  erclwwlkntr  30644  clwwlknonex2  30682  uhgr3cyclex  30765  upgr4cycl4dv4e  30768  eucrctshift  30826  3cyclfrgrrn1  30868  frgrwopreglem2  30896  frgrwopreglem5  30904  frgrwopreglem5ALT  30905  numclwwlk1lem2fo  30941  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  frgrreg  30977  friendshipgt3  30981  friendship  30982  ipasslem1  31415  shmodsi  31973  elspansn5  32158  h1datomi  32165  nmopsetretALT  32447  pjss2coi  32748  pj3cor1i  32793  mdexchi  32919  atcvat4i  32981  mdsymlem3  32989  mdsymlem4  32990  sumdmdii  32999  cdj3lem2b  33021  elabreximd  33088  iuninc  33137  iundisjf  33165  xrsmulgzz  33552  gsumvsca1  33769  gsumvsca2  33770  unitprodclb  33926  rprmdvdsprod  34048  1arithidom  34051  constrmon  34358  locfinreflem  34454  xrge0iifiso  34549  lmxrge0  34566  esumfzf  34683  sigaclfu2  34735  signstfvneq0  35184  satfrel  36101  satfrnmapom  36104  fmlafvel  36119  fmlasuc  36120  bccolsum  36473  faclimlem1  36477  segletr  36849  segleantisym  36850  outsideoftr  36864  exp5d  37061  elicc3  37075  mh-inf3f1  37299  finxpreclem2  38281  wl-sbcom2d  38461  poimirlem26  38532  mblfinlem3  38545  itg2addnc  38560  indexa  38635  disjlem19  39804  ax12indalem  39970  ax12inda2ALT  39971  cvrat4  40468  elpaddn0  40825  paddasslem5  40849  paddasslem14  40858  eldioph2  43726  pell1234qrdich  43821  oaabsb  44254  onmcl  44291  tfsconcat0b  44306  oaun3lem1  44334  oaun3lem2  44335  naddgeoa  44354  gneispb  45090  rexlimd3  46102  rexabslelem  46372  climsuselem1  46563  stoweidlem19  46973  stoweidlem20  46974  stoweidlem34  46988  wallispilem3  47021  sge0iunmpt  47372  meaiuninc3v  47438  smflimmpt  47764  or2expropbilem1  48046  fsetprcnexALT  48076  2reu8i  48127  2elfz2melfz  48332  subsubelfzo0  48341  iccpartigtl  48449  iccpartgt  48453  icceuelpartlem  48461  fargshiftf1  48467  ich2exprop  48497  ichreuopeq  48499  lighneallem3  48636  gbowgt5  48804  bgoldbtbndlem3  48849  bgoldbtbndlem4  48850  bgoldbtbnd  48851  tgblthelfgott  48857  grimco  48931  isuspgrimlem  48937  grimedg  48977  upgrwlkupwlk  49182  2zrngagrp  49290  lmodvsmdi  49435  ply1mulgsumlem1  49442  elfzolborelfzop1  49575  nnolog2flm1  49646  nn0sumshdiglemA  49675  eenglngeehlnmlem2  49794