Theorem exp31 424

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp41  439  exp42  440  imp5a  445  expl  462  anasss  471  an31s  666  exbiri  822  3exp  1135  exp516  1373  rexlimdva2  3168  r19.29af2  3273  reusv2lem2  5360  pwssun  5543  onmindif  6444  mpteqb  6999  dffo3f  7091  fompt  7103  fliftfun  7300  elovmpt3rab1  7660  ordsucss  7802  tfindsg  7845  tfrlem1  8350  tfrlem9  8360  oaordi  8519  oaordex  8531  oaass  8534  oarec  8535  omass  8553  oen0  8560  oeordsuc  8568  nnaordi  8592  omsmolem  8631  naddssim  8660  brinxper  8712  infensuc  9131  suppeqfsuppbi  9327  marypha1lem  9381  hartogs  9494  card2on  9504  tz9.12lem3  9749  infxpenlem  9985  cfcoflem  10244  isf32lem12  10336  zorn2lem6  10473  ondomon  10535  axrepnd  10567  fpwwe2lem11  10614  genpcd  10979  ltexprlem6  11014  axpre-sup  11142  negf1o  11632  recex  11834  uzaddcl  12916  nn01to3  12953  rpnnen1lem5  12993  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  supxrunb2  13334  fz0fzelfz0  13650  fz0fzdiffz0  13653  elfzmlbp  13655  difelfzle  13657  fzo1fzo0n0  13732  elincfzoext  13740  ssfzo12bi  13778  elfznelfzo  13790  modaddmodup  13958  modfzo0difsn  13967  fsuppmapnn0fiubex  14016  seqf1o  14067  expcllem  14096  expeq0  14116  mulexp  14125  hashgt12el2  14448  hashimarni  14466  hash2prd  14500  fi1uzind  14532  swrdnd  14680  swrdswrdlem  14729  swrdswrd  14730  pfxccat3  14759  reuccatpfxs1  14772  repswswrd  14809  repswccat  14811  cshwidxmod  14828  2cshwcshw  14850  s4f1o  14943  wwlktovfo  14983  relexpindlem  15088  resqrex  15289  summo  15756  fsum2d  15810  modfsummods  15833  binom  15872  clim2prod  15930  fprod2d  16023  binomfallfac  16083  efexp  16145  demoivreALT  16245  divconjdvds  16361  addmodlteqALT  16371  dfgcd2  16592  lcmfunsnlem2lem1  16684  lcmfdvdsb  16689  lcmfun  16691  coprmprod  16707  coprmproddvdslem  16708  oddprmdvds  16951  ramcl  17077  prmgaplem6  17104  cshwsidrepswmod0  17142  cshwshashlem1  17143  cshwshashlem2  17144  ressress  17295  initoeu2lem1  18059  symggen  19528  pmtr3ncom  19533  gsumle  20203  srgmulgass  20287  srgbinom  20301  ringinvnzdiv  20372  rhmsubcrngclem2  20740  lmodvsmmulgdi  20984  nzerooringczr  21587  ofldchr  21683  psgndiflemB  21707  assamulgscmlem2  22007  mptcoe1fsupp  22332  coe1fzgsumdlem  22420  evl1gsumdlem  22473  scmatmulcl  22632  mdetdiagid  22714  pm2mpf1  22913  mptcoe1matfsupp  22916  mp2pm2mplem4  22923  chpdmat  22955  chfacfisf  22968  chfacfisfcpmat  22969  chcoeffeq  23000  topbas  23086  elcls  23187  elcls3  23197  2ndcdisj  23570  filufint  24034  ovoliunlem3  25620  dvge0  26122  ulmcn  26516  gausslemma2dlem3  27486  nosupbnd1  27832  nosupbnd2  27834  noinfbnd1  27847  noinfbnd2  27849  sizusglecusg  29718  upgriswlk  29895  2pthnloop  29985  crctcshwlkn0  30075  wlknwwlksnbij  30142  wwlksnred  30146  wwlksnext  30147  wwlksnextinj  30153  wwlksnextproplem2  30164  wwlksnextproplem3  30165  usgr2wspthons3  30221  clwwlkccatlem  30245  clwlkclwwlklem2a4  30253  clwlkclwwlklem2a  30254  clwlkclwwlklem2  30256  erclwwlktr  30278  clwwlkinwwlk  30296  clwwlkf  30303  clwwlkf1  30305  wwlksext2clwwlk  30313  clwwlknscsh  30318  umgr2cwwk2dif  30320  erclwwlkntr  30327  clwwlknonex2  30365  uhgr3cyclex  30438  upgr4cycl4dv4e  30441  eucrctshift  30499  3cyclfrgrrn1  30541  frgrwopreglem2  30569  frgrwopreglem5  30577  frgrwopreglem5ALT  30578  numclwwlk1lem2fo  30614  numclwlk2lem2f  30633  numclwlk2lem2f1o  30635  frgrreg  30650  friendshipgt3  30654  friendship  30655  ipasslem1  31088  shmodsi  31646  elspansn5  31831  h1datomi  31838  nmopsetretALT  32120  pjss2coi  32421  pj3cor1i  32466  mdexchi  32592  atcvat4i  32654  mdsymlem3  32662  mdsymlem4  32663  sumdmdii  32672  cdj3lem2b  32694  elabreximd  32762  iuninc  32811  iundisjf  32840  xrsmulgzz  33237  gsumvsca1  33454  gsumvsca2  33455  unitprodclb  33613  rprmdvdsprod  33736  1arithidom  33739  constrmon  34046  locfinreflem  34142  xrge0iifiso  34237  lmxrge0  34254  esumfzf  34371  sigaclfu2  34423  signstfvneq0  34871  satfrel  35725  satfrnmapom  35728  fmlafvel  35743  fmlasuc  35744  bccolsum  36097  faclimlem1  36101  segletr  36472  segleantisym  36473  outsideoftr  36487  exp5d  36670  elicc3  36685  finxpreclem2  37891  wl-sbcom2d  38071  poimirlem26  38152  mblfinlem3  38165  itg2addnc  38180  indexa  38239  disjlem19  39410  ax12indalem  39576  ax12inda2ALT  39577  cvrat4  40074  elpaddn0  40431  paddasslem5  40455  paddasslem14  40464  eldioph2  43350  pell1234qrdich  43445  oaabsb  43878  onmcl  43915  tfsconcat0b  43930  oaun3lem1  43958  oaun3lem2  43959  naddgeoa  43978  gneispb  44714  rexlimd3  45721  rexabslelem  45991  climsuselem1  46182  stoweidlem19  46592  stoweidlem20  46593  stoweidlem34  46607  wallispilem3  46640  sge0iunmpt  46991  meaiuninc3v  47057  smflimmpt  47383  or2expropbilem1  47625  fsetprcnexALT  47655  2reu8i  47706  2elfz2melfz  47911  subsubelfzo0  47920  iccpartigtl  48028  iccpartgt  48032  icceuelpartlem  48040  fargshiftf1  48046  ich2exprop  48076  ichreuopeq  48078  lighneallem3  48215  gbowgt5  48383  bgoldbtbndlem3  48428  bgoldbtbndlem4  48429  bgoldbtbnd  48430  tgblthelfgott  48436  grimco  48510  isuspgrimlem  48516  grimedg  48556  upgrwlkupwlk  48761  2zrngagrp  48870  lmodvsmdi  49011  ply1mulgsumlem1  49018  elfzolborelfzop1  49151  nnolog2flm1  49222  nn0sumshdiglemA  49251  eenglngeehlnmlem2  49370