Theorem exp31 421

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  exp41  436  exp42  437  imp5a  442  expl  459  anasss  468  an31s  653  exbiri  810  3exp  1120  exp516  1357  rexlimdva2  3158  r19.29af2  3265  reusv2lem2  5398  pwssun  5572  onmindif  6457  mpteqb  7018  fliftfun  7309  elovmpt3rab1  7666  ordsucss  7806  tfindsg  7850  tfrlem1  8376  tfrlem9  8385  oaordi  8546  oaordex  8558  oaass  8561  oarec  8562  omass  8580  oen0  8586  oeordsuc  8594  nnaordi  8618  omsmolem  8656  naddssim  8684  infensuc  9155  php3OLD  9224  suppeqfsuppbi  9377  marypha1lem  9428  hartogs  9539  card2on  9549  tz9.12lem3  9784  infxpenlem  10008  cfcoflem  10267  isf32lem12  10359  zorn2lem6  10496  ondomon  10558  axrepnd  10589  fpwwe2lem11  10636  genpcd  11001  ltexprlem6  11036  axpre-sup  11164  negf1o  11644  recex  11846  uzaddcl  12888  nn01to3  12925  rpnnen1lem5  12965  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  supxrunb2  13299  fz0fzelfz0  13607  fz0fzdiffz0  13610  elfzmlbp  13612  difelfzle  13614  fzo1fzo0n0  13683  elincfzoext  13690  ssfzo12bi  13727  elfznelfzo  13737  modaddmodup  13899  modfzo0difsn  13908  fsuppmapnn0fiubex  13957  seqf1o  14009  expcllem  14038  expeq0  14058  mulexp  14067  hashgt12el2  14383  hashimarni  14401  hash2prd  14436  fi1uzind  14458  swrdnd  14604  swrdswrdlem  14654  swrdswrd  14655  pfxccat3  14684  reuccatpfxs1  14697  repswswrd  14734  repswccat  14736  cshwidxmod  14753  2cshwcshw  14776  s4f1o  14869  wwlktovfo  14909  relexpindlem  15010  resqrex  15197  summo  15663  fsum2d  15717  modfsummods  15739  binom  15776  clim2prod  15834  fprod2d  15925  binomfallfac  15985  efexp  16044  demoivreALT  16144  divconjdvds  16258  addmodlteqALT  16268  dfgcd2  16488  lcmfunsnlem2lem1  16575  lcmfdvdsb  16580  lcmfun  16582  coprmprod  16598  coprmproddvdslem  16599  oddprmdvds  16836  ramcl  16962  prmgaplem6  16989  cshwsidrepswmod0  17028  cshwshashlem1  17029  cshwshashlem2  17030  ressress  17193  initoeu2lem1  17964  symggen  19338  pmtr3ncom  19343  srgmulgass  20040  srgbinom  20054  ringinvnzdiv  20113  lmodvsmmulgdi  20507  psgndiflemB  21153  assamulgscmlem2  21454  mptcoe1fsupp  21739  coe1fzgsumdlem  21825  evl1gsumdlem  21875  scmatmulcl  22020  mdetdiagid  22102  pm2mpf1  22301  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  chpdmat  22343  chfacfisf  22356  chfacfisfcpmat  22357  chcoeffeq  22388  topbas  22475  elcls  22577  elcls3  22587  2ndcdisj  22960  filufint  23424  ovoliunlem3  25021  dvge0  25523  ulmcn  25911  gausslemma2dlem3  26871  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  sizusglecusg  28720  upgriswlk  28898  2pthnloop  28988  crctcshwlkn0  29075  wlknwwlksnbij  29142  wwlksnred  29146  wwlksnext  29147  wwlksnextinj  29153  wwlksnextproplem2  29164  wwlksnextproplem3  29165  usgr2wspthons3  29218  clwwlkccatlem  29242  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  erclwwlktr  29275  clwwlkinwwlk  29293  clwwlkf  29300  clwwlkf1  29302  wwlksext2clwwlk  29310  clwwlknscsh  29315  umgr2cwwk2dif  29317  erclwwlkntr  29324  clwwlknonex2  29362  uhgr3cyclex  29435  upgr4cycl4dv4e  29438  eucrctshift  29496  3cyclfrgrrn1  29538  frgrwopreglem2  29566  frgrwopreglem5  29574  frgrwopreglem5ALT  29575  numclwwlk1lem2fo  29611  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  frgrreg  29647  friendshipgt3  29651  friendship  29652  ipasslem1  30084  shmodsi  30642  elspansn5  30827  h1datomi  30834  nmopsetretALT  31116  pjss2coi  31417  pj3cor1i  31462  mdexchi  31588  atcvat4i  31650  mdsymlem3  31658  mdsymlem4  31659  sumdmdii  31668  cdj3lem2b  31690  elabreximd  31747  iuninc  31792  iundisjf  31820  xrsmulgzz  32179  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  ofldchr  32432  locfinreflem  32820  xrge0iifiso  32915  lmxrge0  32932  esumfzf  33067  sigaclfu2  33119  signstfvneq0  33583  satfrel  34358  satfrnmapom  34361  fmlafvel  34376  fmlasuc  34377  bccolsum  34709  faclimlem1  34713  segletr  35086  segleantisym  35087  outsideoftr  35101  exp5d  35187  elicc3  35202  finxpreclem2  36271  wl-sbcom2d  36426  poimirlem26  36514  mblfinlem3  36527  itg2addnc  36542  indexa  36601  disjlem19  37671  ax12indalem  37815  ax12inda2ALT  37816  cvrat4  38314  elpaddn0  38671  paddasslem5  38695  paddasslem14  38704  eldioph2  41500  pell1234qrdich  41599  oaabsb  42044  onmcl  42081  tfsconcat0b  42096  oaun3lem1  42124  oaun3lem2  42125  naddgeoa  42145  gneispb  42882  rexlimd3  43833  rexabslelem  44128  climsuselem1  44323  stoweidlem19  44735  stoweidlem20  44736  stoweidlem34  44750  wallispilem3  44783  sge0iunmpt  45134  meaiuninc3v  45200  smflimmpt  45526  or2expropbilem1  45742  fsetprcnexALT  45772  2reu8i  45821  2elfz2melfz  46026  subsubelfzo0  46034  iccpartigtl  46091  iccpartgt  46095  icceuelpartlem  46103  fargshiftf1  46109  ich2exprop  46139  ichreuopeq  46141  lighneallem3  46275  gbowgt5  46430  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  tgblthelfgott  46483  isomuspgrlem2b  46497  upgrwlkupwlk  46518  2zrngagrp  46841  rhmsubcrngclem2  46926  nzerooringczr  46970  lmodvsmdi  47058  ply1mulgsumlem1  47067  elfzolborelfzop1  47200  nnolog2flm1  47276  nn0sumshdiglemA  47305  eenglngeehlnmlem2  47424