Theorem exp31 422

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp41  437  exp42  438  imp5a  443  expl  460  anasss  469  an31s  652  exbiri  809  3exp  1115  exp516  1352  rexlimdva2  3287  r19.29af2  3330  reusv2lem2  5300  pwssun  5456  onmindif  6280  mpteqb  6787  fliftfun  7065  elovmpt3rab1  7405  ordsucss  7533  tfindsg  7575  imacosuppOLD  7875  tfrlem1  8012  tfrlem9  8021  oaordi  8172  oaordex  8184  oaass  8187  oarec  8188  omass  8206  oen0  8212  oeordsuc  8220  nnaordi  8244  omsmolem  8280  infensuc  8695  php3  8703  suppeqfsuppbi  8847  marypha1lem  8897  hartogs  9008  card2on  9018  tz9.12lem3  9218  infxpenlem  9439  cfcoflem  9694  isf32lem12  9786  zorn2lem6  9923  ondomon  9985  axrepnd  10016  fpwwe2lem12  10063  genpcd  10428  ltexprlem6  10463  axpre-sup  10591  negf1o  11070  recex  11272  fiminreOLD  11590  uzaddcl  12305  nn01to3  12342  rpnnen1lem5  12381  xrsupsslem  12701  xrinfmsslem  12702  supxrunb1  12713  supxrunb2  12714  fz0fzelfz0  13014  fz0fzdiffz0  13017  elfzmlbp  13019  difelfzle  13021  fzo1fzo0n0  13089  elincfzoext  13096  ssfzo12bi  13133  elfznelfzo  13143  modaddmodup  13303  modfzo0difsn  13312  fsuppmapnn0fiubex  13361  seqf1o  13412  expcllem  13441  expeq0  13460  mulexp  13469  hashgt12el2  13785  hashimarni  13803  hash2prd  13834  fi1uzind  13856  swrdnd  14016  swrdswrdlem  14066  swrdswrd  14067  pfxccat3  14096  reuccatpfxs1  14109  repswswrd  14146  repswccat  14148  cshwidxmod  14165  2cshwcshw  14187  s4f1o  14280  wwlktovfo  14322  resqrex  14610  summo  15074  fsum2d  15126  modfsummods  15148  binom  15185  clim2prod  15244  fprod2d  15335  binomfallfac  15395  efexp  15454  demoivreALT  15554  divconjdvds  15665  addmodlteqALT  15675  dfgcd2  15894  lcmfunsnlem2lem1  15982  lcmfdvdsb  15987  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  oddprmdvds  16239  ramcl  16365  prmgaplem6  16392  cshwsidrepswmod0  16428  cshwshashlem1  16429  cshwshashlem2  16430  ressress  16562  initoeu2lem1  17274  symggen  18598  pmtr3ncom  18603  srgmulgass  19281  srgbinom  19295  ringinvnzdiv  19343  lmodvsmmulgdi  19669  assamulgscmlem2  20129  mptcoe1fsupp  20383  coe1fzgsumdlem  20469  evl1gsumdlem  20519  psgndiflemB  20744  scmatmulcl  21127  mdetdiagid  21209  pm2mpf1  21407  mptcoe1matfsupp  21410  mp2pm2mplem4  21417  chpdmat  21449  chfacfisf  21462  chfacfisfcpmat  21463  chcoeffeq  21494  topbas  21580  elcls  21681  elcls3  21691  2ndcdisj  22064  filufint  22528  ovoliunlem3  24105  dvge0  24603  ulmcn  24987  gausslemma2dlem3  25944  sizusglecusg  27245  upgriswlk  27422  2pthnloop  27512  crctcshwlkn0  27599  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnext  27671  wwlksnextinj  27677  wwlksnextproplem2  27689  wwlksnextproplem3  27690  usgr2wspthons3  27743  clwwlkccatlem  27767  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  erclwwlktr  27800  clwwlkinwwlk  27818  clwwlkf  27826  clwwlkf1  27828  wwlksext2clwwlk  27836  clwwlknscsh  27841  umgr2cwwk2dif  27843  erclwwlkntr  27850  clwwlknonex2  27888  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  eucrctshift  28022  3cyclfrgrrn1  28064  frgrwopreglem2  28092  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  numclwwlk1lem2fo  28137  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  frgrreg  28173  friendshipgt3  28177  friendship  28178  ipasslem1  28608  shmodsi  29166  elspansn5  29351  h1datomi  29358  nmopsetretALT  29640  pjss2coi  29941  pj3cor1i  29986  mdexchi  30112  atcvat4i  30174  mdsymlem3  30182  mdsymlem4  30183  sumdmdii  30192  cdj3lem2b  30214  elabreximd  30270  iuninc  30312  iundisjf  30339  xrsmulgzz  30665  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  ofldchr  30887  locfinreflem  31104  xrge0iifiso  31178  lmxrge0  31195  esumfzf  31328  sigaclfu2  31380  signstfvneq0  31842  satfrel  32614  satfrnmapom  32617  fmlafvel  32632  fmlasuc  32633  bccolsum  32971  faclimlem1  32975  dftrpred3g  33072  nosupbnd1  33214  nosupbnd2  33216  segletr  33575  segleantisym  33576  outsideoftr  33590  exp5d  33650  elicc3  33665  finxpreclem2  34674  wl-sbcom2d  34812  poimirlem26  34933  mblfinlem3  34946  itg2addnc  34961  indexa  35023  ax12indalem  36096  ax12inda2ALT  36097  cvrat4  36594  elpaddn0  36951  paddasslem5  36975  paddasslem14  36984  eldioph2  39408  pell1234qrdich  39507  gneispb  40530  rexlimd3  41462  rexabslelem  41741  climsuselem1  41937  stoweidlem19  42353  stoweidlem20  42354  stoweidlem34  42368  wallispilem3  42401  sge0iunmpt  42749  meaiuninc3v  42815  smflimmpt  43133  or2expropbilem1  43316  2reu8i  43361  2elfz2melfz  43567  subsubelfzo0  43575  iccpartigtl  43632  iccpartgt  43636  icceuelpartlem  43644  fargshiftf1  43650  ich2exprop  43682  ichreuopeq  43684  lighneallem3  43821  gbowgt5  43976  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  tgblthelfgott  44029  isomuspgrlem2b  44043  upgrwlkupwlk  44064  2zrngagrp  44263  rhmsubcrngclem2  44348  nzerooringczr  44392  lmodvsmdi  44479  ply1mulgsumlem1  44489  elfzolborelfzop1  44623  nnolog2flm1  44699  nn0sumshdiglemA  44728  eenglngeehlnmlem2  44774