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  655  exbiri  811  3exp  1120  exp516  1358  rexlimdva2  3140  r19.29af2  3245  reusv2lem2  5341  pwssun  5523  onmindif  6417  mpteqb  6967  dffo3f  7058  fompt  7070  fliftfun  7267  elovmpt3rab1  7627  ordsucss  7769  tfindsg  7812  tfrlem1  8315  tfrlem9  8324  oaordi  8481  oaordex  8493  oaass  8496  oarec  8497  omass  8515  oen0  8522  oeordsuc  8530  nnaordi  8554  omsmolem  8593  naddssim  8621  brinxper  8673  infensuc  9093  suppeqfsuppbi  9292  marypha1lem  9346  hartogs  9459  card2on  9469  tz9.12lem3  9713  infxpenlem  9935  cfcoflem  10194  isf32lem12  10286  zorn2lem6  10423  ondomon  10485  axrepnd  10517  fpwwe2lem11  10564  genpcd  10929  ltexprlem6  10964  axpre-sup  11092  negf1o  11580  recex  11782  uzaddcl  12854  nn01to3  12891  rpnnen1lem5  12931  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  fz0fzelfz0  13588  fz0fzdiffz0  13591  elfzmlbp  13593  difelfzle  13595  fzo1fzo0n0  13670  elincfzoext  13678  ssfzo12bi  13716  elfznelfzo  13728  modaddmodup  13896  modfzo0difsn  13905  fsuppmapnn0fiubex  13954  seqf1o  14005  expcllem  14034  expeq0  14054  mulexp  14063  hashgt12el2  14385  hashimarni  14403  hash2prd  14437  fi1uzind  14469  swrdnd  14617  swrdswrdlem  14666  swrdswrd  14667  pfxccat3  14696  reuccatpfxs1  14709  repswswrd  14746  repswccat  14748  cshwidxmod  14765  2cshwcshw  14787  s4f1o  14880  wwlktovfo  14920  relexpindlem  15025  resqrex  15212  summo  15679  fsum2d  15733  modfsummods  15756  binom  15795  clim2prod  15853  fprod2d  15946  binomfallfac  16006  efexp  16068  demoivreALT  16168  divconjdvds  16284  addmodlteqALT  16294  dfgcd2  16515  lcmfunsnlem2lem1  16607  lcmfdvdsb  16612  lcmfun  16614  coprmprod  16630  coprmproddvdslem  16631  oddprmdvds  16874  ramcl  17000  prmgaplem6  17027  cshwsidrepswmod0  17065  cshwshashlem1  17066  cshwshashlem2  17067  ressress  17217  initoeu2lem1  17981  symggen  19445  pmtr3ncom  19450  gsumle  20120  srgmulgass  20198  srgbinom  20212  ringinvnzdiv  20282  rhmsubcrngclem2  20644  lmodvsmmulgdi  20892  nzerooringczr  21460  ofldchr  21556  psgndiflemB  21580  assamulgscmlem2  21880  mptcoe1fsupp  22179  coe1fzgsumdlem  22268  evl1gsumdlem  22321  scmatmulcl  22483  mdetdiagid  22565  pm2mpf1  22764  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chpdmat  22806  chfacfisf  22819  chfacfisfcpmat  22820  chcoeffeq  22851  topbas  22937  elcls  23038  elcls3  23048  2ndcdisj  23421  filufint  23885  ovoliunlem3  25471  dvge0  25973  ulmcn  26364  gausslemma2dlem3  27331  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  sizusglecusg  29532  upgriswlk  29709  2pthnloop  29799  crctcshwlkn0  29889  wlknwwlksnbij  29956  wwlksnred  29960  wwlksnext  29961  wwlksnextinj  29967  wwlksnextproplem2  29978  wwlksnextproplem3  29979  usgr2wspthons3  30035  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  erclwwlktr  30092  clwwlkinwwlk  30110  clwwlkf  30117  clwwlkf1  30119  wwlksext2clwwlk  30127  clwwlknscsh  30132  umgr2cwwk2dif  30134  erclwwlkntr  30141  clwwlknonex2  30179  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  eucrctshift  30313  3cyclfrgrrn1  30355  frgrwopreglem2  30383  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  numclwwlk1lem2fo  30428  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  frgrreg  30464  friendshipgt3  30468  friendship  30469  ipasslem1  30902  shmodsi  31460  elspansn5  31645  h1datomi  31652  nmopsetretALT  31934  pjss2coi  32235  pj3cor1i  32280  mdexchi  32406  atcvat4i  32468  mdsymlem3  32476  mdsymlem4  32477  sumdmdii  32486  cdj3lem2b  32508  elabreximd  32580  iuninc  32630  iundisjf  32659  xrsmulgzz  33069  gsumvsca1  33287  gsumvsca2  33288  unitprodclb  33449  rprmdvdsprod  33594  1arithidom  33597  constrmon  33888  locfinreflem  33984  xrge0iifiso  34079  lmxrge0  34096  esumfzf  34213  sigaclfu2  34265  signstfvneq0  34716  satfrel  35549  satfrnmapom  35552  fmlafvel  35567  fmlasuc  35568  bccolsum  35921  faclimlem1  35925  segletr  36296  segleantisym  36297  outsideoftr  36311  exp5d  36484  elicc3  36499  finxpreclem2  37706  wl-sbcom2d  37886  poimirlem26  37967  mblfinlem3  37980  itg2addnc  37995  indexa  38054  disjlem19  39225  ax12indalem  39391  ax12inda2ALT  39392  cvrat4  39889  elpaddn0  40246  paddasslem5  40270  paddasslem14  40279  eldioph2  43194  pell1234qrdich  43289  oaabsb  43722  onmcl  43759  tfsconcat0b  43774  oaun3lem1  43802  oaun3lem2  43803  naddgeoa  43822  gneispb  44558  rexlimd3  45574  rexabslelem  45846  climsuselem1  46037  stoweidlem19  46447  stoweidlem20  46448  stoweidlem34  46462  wallispilem3  46495  sge0iunmpt  46846  meaiuninc3v  46912  smflimmpt  47238  or2expropbilem1  47480  fsetprcnexALT  47510  2reu8i  47561  2elfz2melfz  47766  subsubelfzo0  47775  iccpartigtl  47883  iccpartgt  47887  icceuelpartlem  47895  fargshiftf1  47901  ich2exprop  47931  ichreuopeq  47933  lighneallem3  48070  gbowgt5  48238  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgblthelfgott  48291  grimco  48365  isuspgrimlem  48371  grimedg  48411  upgrwlkupwlk  48616  2zrngagrp  48725  lmodvsmdi  48855  ply1mulgsumlem1  48862  elfzolborelfzop1  48995  nnolog2flm1  49066  nn0sumshdiglemA  49095  eenglngeehlnmlem2  49214