Theorem exp31 420

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  exp41  435  exp42  436  imp5a  441  expl  458  anasss  467  an31s  651  exbiri  808  3exp  1118  exp516  1355  rexlimdva2  3217  r19.29af2  3262  reusv2lem2  5323  pwssun  5486  onmindif  6359  mpteqb  6903  fliftfun  7192  elovmpt3rab1  7538  ordsucss  7674  tfindsg  7716  tfrlem1  8216  tfrlem9  8225  oaordi  8386  oaordex  8398  oaass  8401  oarec  8402  omass  8420  oen0  8426  oeordsuc  8434  nnaordi  8458  omsmolem  8496  infensuc  8951  php3OLD  9016  suppeqfsuppbi  9151  marypha1lem  9201  hartogs  9312  card2on  9322  tz9.12lem3  9556  infxpenlem  9778  cfcoflem  10037  isf32lem12  10129  zorn2lem6  10266  ondomon  10328  axrepnd  10359  fpwwe2lem11  10406  genpcd  10771  ltexprlem6  10806  axpre-sup  10934  negf1o  11414  recex  11616  uzaddcl  12653  nn01to3  12690  rpnnen1lem5  12730  xrsupsslem  13050  xrinfmsslem  13051  supxrunb1  13062  supxrunb2  13063  fz0fzelfz0  13371  fz0fzdiffz0  13374  elfzmlbp  13376  difelfzle  13378  fzo1fzo0n0  13447  elincfzoext  13454  ssfzo12bi  13491  elfznelfzo  13501  modaddmodup  13663  modfzo0difsn  13672  fsuppmapnn0fiubex  13721  seqf1o  13773  expcllem  13802  expeq0  13822  mulexp  13831  hashgt12el2  14147  hashimarni  14165  hash2prd  14198  fi1uzind  14220  swrdnd  14376  swrdswrdlem  14426  swrdswrd  14427  pfxccat3  14456  reuccatpfxs1  14469  repswswrd  14506  repswccat  14508  cshwidxmod  14525  2cshwcshw  14547  s4f1o  14640  wwlktovfo  14682  relexpindlem  14783  resqrex  14971  summo  15438  fsum2d  15492  modfsummods  15514  binom  15551  clim2prod  15609  fprod2d  15700  binomfallfac  15760  efexp  15819  demoivreALT  15919  divconjdvds  16033  addmodlteqALT  16043  dfgcd2  16263  lcmfunsnlem2lem1  16352  lcmfdvdsb  16357  lcmfun  16359  coprmprod  16375  coprmproddvdslem  16376  oddprmdvds  16613  ramcl  16739  prmgaplem6  16766  cshwsidrepswmod0  16805  cshwshashlem1  16806  cshwshashlem2  16807  ressress  16967  initoeu2lem1  17738  symggen  19087  pmtr3ncom  19092  srgmulgass  19776  srgbinom  19790  ringinvnzdiv  19841  lmodvsmmulgdi  20167  psgndiflemB  20814  assamulgscmlem2  21113  mptcoe1fsupp  21395  coe1fzgsumdlem  21481  evl1gsumdlem  21531  scmatmulcl  21676  mdetdiagid  21758  pm2mpf1  21957  mptcoe1matfsupp  21960  mp2pm2mplem4  21967  chpdmat  21999  chfacfisf  22012  chfacfisfcpmat  22013  chcoeffeq  22044  topbas  22131  elcls  22233  elcls3  22243  2ndcdisj  22616  filufint  23080  ovoliunlem3  24677  dvge0  25179  ulmcn  25567  gausslemma2dlem3  26525  sizusglecusg  27839  upgriswlk  28017  2pthnloop  28108  crctcshwlkn0  28195  wlknwwlksnbij  28262  wwlksnred  28266  wwlksnext  28267  wwlksnextinj  28273  wwlksnextproplem2  28284  wwlksnextproplem3  28285  usgr2wspthons3  28338  clwwlkccatlem  28362  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  erclwwlktr  28395  clwwlkinwwlk  28413  clwwlkf  28420  clwwlkf1  28422  wwlksext2clwwlk  28430  clwwlknscsh  28435  umgr2cwwk2dif  28437  erclwwlkntr  28444  clwwlknonex2  28482  uhgr3cyclex  28555  upgr4cycl4dv4e  28558  eucrctshift  28616  3cyclfrgrrn1  28658  frgrwopreglem2  28686  frgrwopreglem5  28694  frgrwopreglem5ALT  28695  numclwwlk1lem2fo  28731  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  frgrreg  28767  friendshipgt3  28771  friendship  28772  ipasslem1  29202  shmodsi  29760  elspansn5  29945  h1datomi  29952  nmopsetretALT  30234  pjss2coi  30535  pj3cor1i  30580  mdexchi  30706  atcvat4i  30768  mdsymlem3  30776  mdsymlem4  30777  sumdmdii  30786  cdj3lem2b  30808  elabreximd  30864  iuninc  30909  iundisjf  30937  xrsmulgzz  31296  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  ofldchr  31522  locfinreflem  31799  xrge0iifiso  31894  lmxrge0  31911  esumfzf  32046  sigaclfu2  32098  signstfvneq0  32560  satfrel  33338  satfrnmapom  33341  fmlafvel  33356  fmlasuc  33357  bccolsum  33714  faclimlem1  33718  naddssim  33846  nosupbnd1  33926  nosupbnd2  33928  noinfbnd1  33941  noinfbnd2  33943  segletr  34425  segleantisym  34426  outsideoftr  34440  exp5d  34500  elicc3  34515  finxpreclem2  35570  wl-sbcom2d  35725  poimirlem26  35812  mblfinlem3  35825  itg2addnc  35840  indexa  35900  ax12indalem  36966  ax12inda2ALT  36967  cvrat4  37464  elpaddn0  37821  paddasslem5  37845  paddasslem14  37854  eldioph2  40591  pell1234qrdich  40690  gneispb  41748  rexlimd3  42700  rexabslelem  42965  climsuselem1  43155  stoweidlem19  43567  stoweidlem20  43568  stoweidlem34  43582  wallispilem3  43615  sge0iunmpt  43963  meaiuninc3v  44029  smflimmpt  44354  or2expropbilem1  44537  fsetprcnexALT  44567  2reu8i  44616  2elfz2melfz  44821  subsubelfzo0  44829  iccpartigtl  44886  iccpartgt  44890  icceuelpartlem  44898  fargshiftf1  44904  ich2exprop  44934  ichreuopeq  44936  lighneallem3  45070  gbowgt5  45225  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  tgblthelfgott  45278  isomuspgrlem2b  45292  upgrwlkupwlk  45313  2zrngagrp  45512  rhmsubcrngclem2  45597  nzerooringczr  45641  lmodvsmdi  45729  ply1mulgsumlem1  45738  elfzolborelfzop1  45871  nnolog2flm1  45947  nn0sumshdiglemA  45976  eenglngeehlnmlem2  46095