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  5396  pwssun  5570  onmindif  6453  mpteqb  7013  fliftfun  7304  elovmpt3rab1  7661  ordsucss  7801  tfindsg  7845  tfrlem1  8371  tfrlem9  8380  oaordi  8542  oaordex  8554  oaass  8557  oarec  8558  omass  8576  oen0  8582  oeordsuc  8590  nnaordi  8614  omsmolem  8652  naddssim  8680  infensuc  9151  php3OLD  9220  suppeqfsuppbi  9373  marypha1lem  9424  hartogs  9535  card2on  9545  tz9.12lem3  9780  infxpenlem  10004  cfcoflem  10263  isf32lem12  10355  zorn2lem6  10492  ondomon  10554  axrepnd  10585  fpwwe2lem11  10632  genpcd  10997  ltexprlem6  11032  axpre-sup  11160  negf1o  11640  recex  11842  uzaddcl  12884  nn01to3  12921  rpnnen1lem5  12961  xrsupsslem  13282  xrinfmsslem  13283  supxrunb1  13294  supxrunb2  13295  fz0fzelfz0  13603  fz0fzdiffz0  13606  elfzmlbp  13608  difelfzle  13610  fzo1fzo0n0  13679  elincfzoext  13686  ssfzo12bi  13723  elfznelfzo  13733  modaddmodup  13895  modfzo0difsn  13904  fsuppmapnn0fiubex  13953  seqf1o  14005  expcllem  14034  expeq0  14054  mulexp  14063  hashgt12el2  14379  hashimarni  14397  hash2prd  14432  fi1uzind  14454  swrdnd  14600  swrdswrdlem  14650  swrdswrd  14651  pfxccat3  14680  reuccatpfxs1  14693  repswswrd  14730  repswccat  14732  cshwidxmod  14749  2cshwcshw  14772  s4f1o  14865  wwlktovfo  14905  relexpindlem  15006  resqrex  15193  summo  15659  fsum2d  15713  modfsummods  15735  binom  15772  clim2prod  15830  fprod2d  15921  binomfallfac  15981  efexp  16040  demoivreALT  16140  divconjdvds  16254  addmodlteqALT  16264  dfgcd2  16484  lcmfunsnlem2lem1  16571  lcmfdvdsb  16576  lcmfun  16578  coprmprod  16594  coprmproddvdslem  16595  oddprmdvds  16832  ramcl  16958  prmgaplem6  16985  cshwsidrepswmod0  17024  cshwshashlem1  17025  cshwshashlem2  17026  ressress  17189  initoeu2lem1  17960  symggen  19331  pmtr3ncom  19336  srgmulgass  20031  srgbinom  20045  ringinvnzdiv  20103  lmodvsmmulgdi  20495  psgndiflemB  21137  assamulgscmlem2  21436  mptcoe1fsupp  21721  coe1fzgsumdlem  21807  evl1gsumdlem  21857  scmatmulcl  22002  mdetdiagid  22084  pm2mpf1  22283  mptcoe1matfsupp  22286  mp2pm2mplem4  22293  chpdmat  22325  chfacfisf  22338  chfacfisfcpmat  22339  chcoeffeq  22370  topbas  22457  elcls  22559  elcls3  22569  2ndcdisj  22942  filufint  23406  ovoliunlem3  25003  dvge0  25505  ulmcn  25893  gausslemma2dlem3  26851  nosupbnd1  27197  nosupbnd2  27199  noinfbnd1  27212  noinfbnd2  27214  sizusglecusg  28700  upgriswlk  28878  2pthnloop  28968  crctcshwlkn0  29055  wlknwwlksnbij  29122  wwlksnred  29126  wwlksnext  29127  wwlksnextinj  29133  wwlksnextproplem2  29144  wwlksnextproplem3  29145  usgr2wspthons3  29198  clwwlkccatlem  29222  clwlkclwwlklem2a4  29230  clwlkclwwlklem2a  29231  clwlkclwwlklem2  29233  erclwwlktr  29255  clwwlkinwwlk  29273  clwwlkf  29280  clwwlkf1  29282  wwlksext2clwwlk  29290  clwwlknscsh  29295  umgr2cwwk2dif  29297  erclwwlkntr  29304  clwwlknonex2  29342  uhgr3cyclex  29415  upgr4cycl4dv4e  29418  eucrctshift  29476  3cyclfrgrrn1  29518  frgrwopreglem2  29546  frgrwopreglem5  29554  frgrwopreglem5ALT  29555  numclwwlk1lem2fo  29591  numclwlk2lem2f  29610  numclwlk2lem2f1o  29612  frgrreg  29627  friendshipgt3  29631  friendship  29632  ipasslem1  30062  shmodsi  30620  elspansn5  30805  h1datomi  30812  nmopsetretALT  31094  pjss2coi  31395  pj3cor1i  31440  mdexchi  31566  atcvat4i  31628  mdsymlem3  31636  mdsymlem4  31637  sumdmdii  31646  cdj3lem2b  31668  elabreximd  31725  iuninc  31770  iundisjf  31798  xrsmulgzz  32157  gsumle  32220  gsumvsca1  32349  gsumvsca2  32350  ofldchr  32401  locfinreflem  32758  xrge0iifiso  32853  lmxrge0  32870  esumfzf  33005  sigaclfu2  33057  signstfvneq0  33521  satfrel  34296  satfrnmapom  34299  fmlafvel  34314  fmlasuc  34315  bccolsum  34647  faclimlem1  34651  segletr  35024  segleantisym  35025  outsideoftr  35039  exp5d  35125  elicc3  35140  finxpreclem2  36209  wl-sbcom2d  36364  poimirlem26  36452  mblfinlem3  36465  itg2addnc  36480  indexa  36539  disjlem19  37609  ax12indalem  37753  ax12inda2ALT  37754  cvrat4  38252  elpaddn0  38609  paddasslem5  38633  paddasslem14  38642  eldioph2  41433  pell1234qrdich  41532  oaabsb  41977  onmcl  42014  tfsconcat0b  42029  oaun3lem1  42057  oaun3lem2  42058  naddgeoa  42078  gneispb  42815  rexlimd3  43766  rexabslelem  44063  climsuselem1  44258  stoweidlem19  44670  stoweidlem20  44671  stoweidlem34  44685  wallispilem3  44718  sge0iunmpt  45069  meaiuninc3v  45135  smflimmpt  45461  or2expropbilem1  45677  fsetprcnexALT  45707  2reu8i  45756  2elfz2melfz  45961  subsubelfzo0  45969  iccpartigtl  46026  iccpartgt  46030  icceuelpartlem  46038  fargshiftf1  46044  ich2exprop  46074  ichreuopeq  46076  lighneallem3  46210  gbowgt5  46365  bgoldbtbndlem3  46410  bgoldbtbndlem4  46411  bgoldbtbnd  46412  tgblthelfgott  46418  isomuspgrlem2b  46432  upgrwlkupwlk  46453  2zrngagrp  46743  rhmsubcrngclem2  46828  nzerooringczr  46872  lmodvsmdi  46960  ply1mulgsumlem1  46969  elfzolborelfzop1  47102  nnolog2flm1  47178  nn0sumshdiglemA  47207  eenglngeehlnmlem2  47326