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  654  exbiri  810  3exp  1119  exp516  1356  rexlimdva2  3141  r19.29af2  3248  reusv2lem2  5366  pwssun  5542  onmindif  6442  mpteqb  7001  dffo3f  7092  fompt  7104  fliftfun  7300  elovmpt3rab1  7661  ordsucss  7806  tfindsg  7850  tfrlem1  8384  tfrlem9  8393  oaordi  8552  oaordex  8564  oaass  8567  oarec  8568  omass  8586  oen0  8592  oeordsuc  8600  nnaordi  8624  omsmolem  8663  naddssim  8691  brinxper  8742  infensuc  9163  php3OLD  9227  suppeqfsuppbi  9385  marypha1lem  9439  hartogs  9550  card2on  9560  tz9.12lem3  9795  infxpenlem  10019  cfcoflem  10278  isf32lem12  10370  zorn2lem6  10507  ondomon  10569  axrepnd  10600  fpwwe2lem11  10647  genpcd  11012  ltexprlem6  11047  axpre-sup  11175  negf1o  11659  recex  11861  uzaddcl  12912  nn01to3  12949  rpnnen1lem5  12989  xrsupsslem  13315  xrinfmsslem  13316  supxrunb1  13327  supxrunb2  13328  fz0fzelfz0  13640  fz0fzdiffz0  13643  elfzmlbp  13645  difelfzle  13647  fzo1fzo0n0  13720  elincfzoext  13728  ssfzo12bi  13766  elfznelfzo  13777  modaddmodup  13941  modfzo0difsn  13950  fsuppmapnn0fiubex  13999  seqf1o  14050  expcllem  14079  expeq0  14099  mulexp  14108  hashgt12el2  14429  hashimarni  14447  hash2prd  14481  fi1uzind  14513  swrdnd  14659  swrdswrdlem  14709  swrdswrd  14710  pfxccat3  14739  reuccatpfxs1  14752  repswswrd  14789  repswccat  14791  cshwidxmod  14808  2cshwcshw  14831  s4f1o  14924  wwlktovfo  14964  relexpindlem  15069  resqrex  15256  summo  15720  fsum2d  15774  modfsummods  15796  binom  15833  clim2prod  15891  fprod2d  15984  binomfallfac  16044  efexp  16104  demoivreALT  16204  divconjdvds  16319  addmodlteqALT  16329  dfgcd2  16550  lcmfunsnlem2lem1  16642  lcmfdvdsb  16647  lcmfun  16649  coprmprod  16665  coprmproddvdslem  16666  oddprmdvds  16908  ramcl  17034  prmgaplem6  17061  cshwsidrepswmod0  17099  cshwshashlem1  17100  cshwshashlem2  17101  ressress  17253  initoeu2lem1  18012  symggen  19436  pmtr3ncom  19441  srgmulgass  20162  srgbinom  20176  ringinvnzdiv  20246  rhmsubcrngclem2  20612  lmodvsmmulgdi  20839  nzerooringczr  21426  psgndiflemB  21545  assamulgscmlem2  21845  mptcoe1fsupp  22136  coe1fzgsumdlem  22226  evl1gsumdlem  22279  scmatmulcl  22441  mdetdiagid  22523  pm2mpf1  22722  mptcoe1matfsupp  22725  mp2pm2mplem4  22732  chpdmat  22764  chfacfisf  22777  chfacfisfcpmat  22778  chcoeffeq  22809  topbas  22895  elcls  22996  elcls3  23006  2ndcdisj  23379  filufint  23843  ovoliunlem3  25442  dvge0  25948  ulmcn  26345  gausslemma2dlem3  27315  nosupbnd1  27662  nosupbnd2  27664  noinfbnd1  27677  noinfbnd2  27679  sizusglecusg  29375  upgriswlk  29553  2pthnloop  29645  crctcshwlkn0  29735  wlknwwlksnbij  29802  wwlksnred  29806  wwlksnext  29807  wwlksnextinj  29813  wwlksnextproplem2  29824  wwlksnextproplem3  29825  usgr2wspthons3  29878  clwwlkccatlem  29902  clwlkclwwlklem2a4  29910  clwlkclwwlklem2a  29911  clwlkclwwlklem2  29913  erclwwlktr  29935  clwwlkinwwlk  29953  clwwlkf  29960  clwwlkf1  29962  wwlksext2clwwlk  29970  clwwlknscsh  29975  umgr2cwwk2dif  29977  erclwwlkntr  29984  clwwlknonex2  30022  uhgr3cyclex  30095  upgr4cycl4dv4e  30098  eucrctshift  30156  3cyclfrgrrn1  30198  frgrwopreglem2  30226  frgrwopreglem5  30234  frgrwopreglem5ALT  30235  numclwwlk1lem2fo  30271  numclwlk2lem2f  30290  numclwlk2lem2f1o  30292  frgrreg  30307  friendshipgt3  30311  friendship  30312  ipasslem1  30744  shmodsi  31302  elspansn5  31487  h1datomi  31494  nmopsetretALT  31776  pjss2coi  32077  pj3cor1i  32122  mdexchi  32248  atcvat4i  32310  mdsymlem3  32318  mdsymlem4  32319  sumdmdii  32328  cdj3lem2b  32350  elabreximd  32423  iuninc  32474  iundisjf  32503  xrsmulgzz  32920  gsumle  33010  gsumvsca1  33141  gsumvsca2  33142  ofldchr  33254  unitprodclb  33322  rprmdvdsprod  33467  1arithidom  33470  constrmon  33694  locfinreflem  33779  xrge0iifiso  33874  lmxrge0  33891  esumfzf  34008  sigaclfu2  34060  signstfvneq0  34525  satfrel  35310  satfrnmapom  35313  fmlafvel  35328  fmlasuc  35329  bccolsum  35677  faclimlem1  35681  segletr  36053  segleantisym  36054  outsideoftr  36068  exp5d  36241  elicc3  36256  finxpreclem2  37329  wl-sbcom2d  37500  poimirlem26  37591  mblfinlem3  37604  itg2addnc  37619  indexa  37678  disjlem19  38740  ax12indalem  38884  ax12inda2ALT  38885  cvrat4  39383  elpaddn0  39740  paddasslem5  39764  paddasslem14  39773  eldioph2  42710  pell1234qrdich  42809  oaabsb  43243  onmcl  43280  tfsconcat0b  43295  oaun3lem1  43323  oaun3lem2  43324  naddgeoa  43343  gneispb  44080  rexlimd3  45095  rexabslelem  45373  climsuselem1  45566  stoweidlem19  45978  stoweidlem20  45979  stoweidlem34  45993  wallispilem3  46026  sge0iunmpt  46377  meaiuninc3v  46443  smflimmpt  46769  or2expropbilem1  46989  fsetprcnexALT  47019  2reu8i  47070  2elfz2melfz  47275  subsubelfzo0  47283  iccpartigtl  47355  iccpartgt  47359  icceuelpartlem  47367  fargshiftf1  47373  ich2exprop  47403  ichreuopeq  47405  lighneallem3  47539  gbowgt5  47694  bgoldbtbndlem3  47739  bgoldbtbndlem4  47740  bgoldbtbnd  47741  tgblthelfgott  47747  isuspgrimlem  47819  grimco  47825  grimedg  47848  upgrwlkupwlk  48001  2zrngagrp  48110  lmodvsmdi  48240  ply1mulgsumlem1  48248  elfzolborelfzop1  48381  nnolog2flm1  48456  nn0sumshdiglemA  48485  eenglngeehlnmlem2  48604