Theorem exp31 412

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  exp41  427  exp42  428  imp5a  433  expl  451  anasss  460  an31s  644  exbiri  845  3impaOLD  1146  3exp  1152  pm3.2an3OLD  1444  exp516  1469  rexlimdva2  3243  r19.29af2  3285  reusv2lem2  5101  pwssun  5248  onmindif  6056  mpteqb  6551  fliftfun  6822  elovmpt3rab1  7158  ordsucss  7284  tfindsg  7326  imacosupp  7605  tfrlem1  7743  tfrlem9  7752  oaordi  7898  oaordex  7910  oaass  7913  oarec  7914  omass  7932  oen0  7938  oeordsuc  7946  nnaordi  7970  omsmolem  8005  infensuc  8413  php3  8421  suppeqfsuppbi  8564  marypha1lem  8614  hartogs  8725  card2on  8735  tz9.12lem3  8936  infxpenlem  9156  cfcoflem  9416  isf32lem12  9508  zorn2lem6  9645  ondomon  9707  axrepnd  9738  fpwwe2lem12  9785  genpcd  10150  ltexprlem6  10185  axpre-sup  10313  negf1o  10791  recex  10991  uzaddcl  12033  nn01to3  12071  rpnnen1lem5  12110  xrsupsslem  12432  xrinfmsslem  12433  supxrunb1  12444  supxrunb2  12445  fz0fzelfz0  12747  fz0fzdiffz0  12750  elfzmlbp  12752  difelfzle  12754  fzo1fzo0n0  12821  elincfzoext  12828  ssfzo12bi  12865  elfznelfzo  12875  modaddmodup  13035  modfzo0difsn  13044  fsuppmapnn0fiubex  13093  seqf1o  13143  expcllem  13172  expeq0  13191  mulexp  13200  hashgt12el2  13507  hashimarni  13524  hash2prd  13553  fi1uzind  13575  swrdnd  13726  swrdswrdlem  13790  swrdswrd  13791  reuccats1OLD  13825  pfxccat3  13840  swrdccat3OLD  13841  swrdccatidOLD  13852  reuccatpfxs1  13860  repswswrd  13907  repswccat  13909  cshwidxmod  13931  2cshwcshw  13953  s4f1o  14046  wwlktovfo  14087  cjexp  14274  resqrex  14375  absexp  14428  summo  14832  fsum2d  14884  modfsummods  14906  binom  14943  clim2prod  15000  fprod2d  15091  binomfallfac  15151  efexp  15210  demoivreALT  15310  divconjdvds  15421  addmodlteqALT  15431  dfgcd2  15643  lcmfunsnlem2lem1  15731  lcmfdvdsb  15736  lcmfun  15738  coprmprod  15754  coprmproddvdslem  15755  oddprmdvds  15985  ramcl  16111  cshwsidrepswmod0  16174  cshwshashlem1  16175  ressress  16309  initoeu2lem1  17023  symggen  18247  pmtr3ncom  18252  srgmulgass  18892  srgbinom  18906  ringinvnzdiv  18954  lmodvsmmulgdi  19261  assamulgscmlem2  19717  mptcoe1fsupp  19952  coe1fzgsumdlem  20038  evl1gsumdlem  20087  psgndiflemB  20313  scmatmulcl  20699  mdetdiagid  20781  pm2mpf1  20981  mptcoe1matfsupp  20984  mp2pm2mplem4  20991  chpdmat  21023  chfacfisf  21036  chfacfisfcpmat  21037  chcoeffeq  21068  topbas  21154  elcls  21255  elcls3  21265  2ndcdisj  21637  filufint  22101  ovoliunlem3  23677  dvge0  24175  ulmcn  24559  gausslemma2dlem3  25513  sizusglecusg  26768  upgriswlk  26945  2pthnloop  27040  crctcshwlkn0  27127  wlknwwlksnbij  27199  wwlksnred  27209  wwlksnredOLD  27210  wwlksnextinj  27220  wwlksnextinjOLD  27225  wwlksnextproplem2  27241  wwlksnextproplem2OLD  27242  wwlksnextproplem3  27243  wwlksnextproplem3OLD  27244  usgr2wspthons3  27300  clwwlkccatlem  27325  clwlkclwwlklem2a4  27333  clwlkclwwlklem2a  27334  clwlkclwwlklem2  27336  erclwwlktr  27367  clwwlkinwwlk  27385  clwwlkinwwlkOLD  27386  clwwlkfOLD  27393  clwwlkf1OLD  27395  clwwlkf  27398  clwwlkf1  27400  wwlksext2clwwlk  27409  clwwlknscsh  27415  umgr2cwwk2dif  27417  erclwwlkntr  27424  clwlksfclwwlkOLD  27438  clwlksf1clwwlklemOLD  27444  clwwlknonex2  27480  uhgr3cyclex  27554  upgr4cycl4dv4e  27557  eucrctshift  27616  3cyclfrgrrn1  27662  frgrwopreglem2  27690  frgrwopreglem5  27698  frgrwopreglem5ALT  27699  numclwwlk1lem2fo  27745  numclwwlk1lem2foOLD  27750  numclwlk2lem2f  27776  numclwlk2lem2f1o  27778  numclwlk2lem2fOLD  27779  numclwlk2lem2f1oOLD  27781  numclwlk2lem2fOLDOLD  27787  numclwlk2lem2f1oOLDOLD  27789  frgrreg  27805  friendshipgt3  27809  friendship  27810  ipasslem1  28237  shmodsi  28799  elspansn5  28984  h1datomi  28991  nmopsetretALT  29273  pjss2coi  29574  pj3cor1i  29619  mdexchi  29745  atcvat4i  29807  mdsymlem3  29815  mdsymlem4  29816  sumdmdii  29825  cdj3lem2b  29847  elabreximd  29892  iuninc  29922  iundisjf  29945  xrsmulgzz  30219  gsumle  30320  gsumvsca1  30323  gsumvsca2  30324  ofldchr  30355  locfinreflem  30448  xrge0iifiso  30522  lmxrge0  30539  esumfzf  30672  sigaclfu2  30725  signstfvneq0  31193  signstfvc  31195  bccolsum  32163  faclimlem1  32167  dftrpred3g  32266  nosupbnd1  32394  nosupbnd2  32396  segletr  32755  segleantisym  32756  outsideoftr  32770  exp5d  32830  elicc3  32845  finxpreclem2  33767  wl-sbcom2d  33883  poimirlem26  33974  mblfinlem3  33987  itg2addnc  34002  indexa  34066  ax12indalem  35015  ax12inda2ALT  35016  cvrat4  35513  elpaddn0  35870  paddasslem5  35894  paddasslem14  35903  eldioph2  38164  pell1234qrdich  38264  gneispb  39264  rexlimd3  40140  dffo3f  40167  rnmptlb  40248  rexabslelem  40434  climsuselem1  40628  stoweidlem19  41024  stoweidlem20  41025  stoweidlem34  41039  wallispilem3  41072  sge0iunmpt  41420  meaiuninc3v  41486  smflimmpt  41804  2elfz2melfz  42210  subsubelfzo0  42218  iccpartigtl  42241  iccpartgt  42245  icceuelpartlem  42253  fargshiftf1  42259  lighneallem3  42368  gbowgt5  42494  bgoldbtbndlem3  42539  bgoldbtbndlem4  42540  bgoldbtbnd  42541  tgblthelfgott  42547  isomuspgrlem2b  42561  upgrwlkupwlk  42582  2zrngagrp  42804  rhmsubcrngclem2  42889  nzerooringczr  42933  lmodvsmdi  43024  ply1mulgsumlem1  43035  elfzolborelfzop1  43170  nnolog2flm1  43245  nn0sumshdiglemA  43274  eenglngeehlnmlem2  43302