Theorem exp31 420

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  exp41  435  exp42  436  imp5a  441  expl  458  anasss  467  an31s  652  exbiri  809  3exp  1119  exp516  1356  rexlimdva2  3157  r19.29af2  3264  reusv2lem2  5397  pwssun  5571  onmindif  6456  mpteqb  7017  fliftfun  7308  elovmpt3rab1  7665  ordsucss  7805  tfindsg  7849  tfrlem1  8375  tfrlem9  8384  oaordi  8545  oaordex  8557  oaass  8560  oarec  8561  omass  8579  oen0  8585  oeordsuc  8593  nnaordi  8617  omsmolem  8655  naddssim  8683  infensuc  9154  php3OLD  9223  suppeqfsuppbi  9376  marypha1lem  9427  hartogs  9538  card2on  9548  tz9.12lem3  9783  infxpenlem  10007  cfcoflem  10266  isf32lem12  10358  zorn2lem6  10495  ondomon  10557  axrepnd  10588  fpwwe2lem11  10635  genpcd  11000  ltexprlem6  11035  axpre-sup  11163  negf1o  11643  recex  11845  uzaddcl  12887  nn01to3  12924  rpnnen1lem5  12964  xrsupsslem  13285  xrinfmsslem  13286  supxrunb1  13297  supxrunb2  13298  fz0fzelfz0  13606  fz0fzdiffz0  13609  elfzmlbp  13611  difelfzle  13613  fzo1fzo0n0  13682  elincfzoext  13689  ssfzo12bi  13726  elfznelfzo  13736  modaddmodup  13898  modfzo0difsn  13907  fsuppmapnn0fiubex  13956  seqf1o  14008  expcllem  14037  expeq0  14057  mulexp  14066  hashgt12el2  14382  hashimarni  14400  hash2prd  14435  fi1uzind  14457  swrdnd  14603  swrdswrdlem  14653  swrdswrd  14654  pfxccat3  14683  reuccatpfxs1  14696  repswswrd  14733  repswccat  14735  cshwidxmod  14752  2cshwcshw  14775  s4f1o  14868  wwlktovfo  14908  relexpindlem  15009  resqrex  15196  summo  15662  fsum2d  15716  modfsummods  15738  binom  15775  clim2prod  15833  fprod2d  15924  binomfallfac  15984  efexp  16043  demoivreALT  16143  divconjdvds  16257  addmodlteqALT  16267  dfgcd2  16487  lcmfunsnlem2lem1  16574  lcmfdvdsb  16579  lcmfun  16581  coprmprod  16597  coprmproddvdslem  16598  oddprmdvds  16835  ramcl  16961  prmgaplem6  16988  cshwsidrepswmod0  17027  cshwshashlem1  17028  cshwshashlem2  17029  ressress  17192  initoeu2lem1  17963  symggen  19337  pmtr3ncom  19342  srgmulgass  20039  srgbinom  20053  ringinvnzdiv  20112  lmodvsmmulgdi  20506  psgndiflemB  21152  assamulgscmlem2  21453  mptcoe1fsupp  21738  coe1fzgsumdlem  21824  evl1gsumdlem  21874  scmatmulcl  22019  mdetdiagid  22101  pm2mpf1  22300  mptcoe1matfsupp  22303  mp2pm2mplem4  22310  chpdmat  22342  chfacfisf  22355  chfacfisfcpmat  22356  chcoeffeq  22387  topbas  22474  elcls  22576  elcls3  22586  2ndcdisj  22959  filufint  23423  ovoliunlem3  25020  dvge0  25522  ulmcn  25910  gausslemma2dlem3  26868  nosupbnd1  27214  nosupbnd2  27216  noinfbnd1  27229  noinfbnd2  27231  sizusglecusg  28717  upgriswlk  28895  2pthnloop  28985  crctcshwlkn0  29072  wlknwwlksnbij  29139  wwlksnred  29143  wwlksnext  29144  wwlksnextinj  29150  wwlksnextproplem2  29161  wwlksnextproplem3  29162  usgr2wspthons3  29215  clwwlkccatlem  29239  clwlkclwwlklem2a4  29247  clwlkclwwlklem2a  29248  clwlkclwwlklem2  29250  erclwwlktr  29272  clwwlkinwwlk  29290  clwwlkf  29297  clwwlkf1  29299  wwlksext2clwwlk  29307  clwwlknscsh  29312  umgr2cwwk2dif  29314  erclwwlkntr  29321  clwwlknonex2  29359  uhgr3cyclex  29432  upgr4cycl4dv4e  29435  eucrctshift  29493  3cyclfrgrrn1  29535  frgrwopreglem2  29563  frgrwopreglem5  29571  frgrwopreglem5ALT  29572  numclwwlk1lem2fo  29608  numclwlk2lem2f  29627  numclwlk2lem2f1o  29629  frgrreg  29644  friendshipgt3  29648  friendship  29649  ipasslem1  30079  shmodsi  30637  elspansn5  30822  h1datomi  30829  nmopsetretALT  31111  pjss2coi  31412  pj3cor1i  31457  mdexchi  31583  atcvat4i  31645  mdsymlem3  31653  mdsymlem4  31654  sumdmdii  31663  cdj3lem2b  31685  elabreximd  31742  iuninc  31787  iundisjf  31815  xrsmulgzz  32174  gsumle  32237  gsumvsca1  32366  gsumvsca2  32367  ofldchr  32427  locfinreflem  32815  xrge0iifiso  32910  lmxrge0  32927  esumfzf  33062  sigaclfu2  33114  signstfvneq0  33578  satfrel  34353  satfrnmapom  34356  fmlafvel  34371  fmlasuc  34372  bccolsum  34704  faclimlem1  34708  segletr  35081  segleantisym  35082  outsideoftr  35096  exp5d  35182  elicc3  35197  finxpreclem2  36266  wl-sbcom2d  36421  poimirlem26  36509  mblfinlem3  36522  itg2addnc  36537  indexa  36596  disjlem19  37666  ax12indalem  37810  ax12inda2ALT  37811  cvrat4  38309  elpaddn0  38666  paddasslem5  38690  paddasslem14  38699  eldioph2  41490  pell1234qrdich  41589  oaabsb  42034  onmcl  42071  tfsconcat0b  42086  oaun3lem1  42114  oaun3lem2  42115  naddgeoa  42135  gneispb  42872  rexlimd3  43823  rexabslelem  44118  climsuselem1  44313  stoweidlem19  44725  stoweidlem20  44726  stoweidlem34  44740  wallispilem3  44773  sge0iunmpt  45124  meaiuninc3v  45190  smflimmpt  45516  or2expropbilem1  45732  fsetprcnexALT  45762  2reu8i  45811  2elfz2melfz  46016  subsubelfzo0  46024  iccpartigtl  46081  iccpartgt  46085  icceuelpartlem  46093  fargshiftf1  46099  ich2exprop  46129  ichreuopeq  46131  lighneallem3  46265  gbowgt5  46420  bgoldbtbndlem3  46465  bgoldbtbndlem4  46466  bgoldbtbnd  46467  tgblthelfgott  46473  isomuspgrlem2b  46487  upgrwlkupwlk  46508  2zrngagrp  46831  rhmsubcrngclem2  46916  nzerooringczr  46960  lmodvsmdi  47048  ply1mulgsumlem1  47057  elfzolborelfzop1  47190  nnolog2flm1  47266  nn0sumshdiglemA  47295  eenglngeehlnmlem2  47414