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

This theorem is referenced by:  exp41  434  exp42  435  imp5a  440  expl  457  anasss  466  an31s  650  exbiri  807  3exp  1117  exp516  1354  rexlimdva2  3215  r19.29af2  3258  reusv2lem2  5317  pwssun  5476  onmindif  6340  mpteqb  6876  fliftfun  7163  elovmpt3rab1  7507  ordsucss  7640  tfindsg  7682  tfrlem1  8178  tfrlem9  8187  oaordi  8339  oaordex  8351  oaass  8354  oarec  8355  omass  8373  oen0  8379  oeordsuc  8387  nnaordi  8411  omsmolem  8447  infensuc  8891  php3  8899  suppeqfsuppbi  9072  marypha1lem  9122  hartogs  9233  card2on  9243  dftrpred3g  9412  tz9.12lem3  9478  infxpenlem  9700  cfcoflem  9959  isf32lem12  10051  zorn2lem6  10188  ondomon  10250  axrepnd  10281  fpwwe2lem11  10328  genpcd  10693  ltexprlem6  10728  axpre-sup  10856  negf1o  11335  recex  11537  uzaddcl  12573  nn01to3  12610  rpnnen1lem5  12650  xrsupsslem  12970  xrinfmsslem  12971  supxrunb1  12982  supxrunb2  12983  fz0fzelfz0  13291  fz0fzdiffz0  13294  elfzmlbp  13296  difelfzle  13298  fzo1fzo0n0  13366  elincfzoext  13373  ssfzo12bi  13410  elfznelfzo  13420  modaddmodup  13582  modfzo0difsn  13591  fsuppmapnn0fiubex  13640  seqf1o  13692  expcllem  13721  expeq0  13741  mulexp  13750  hashgt12el2  14066  hashimarni  14084  hash2prd  14117  fi1uzind  14139  swrdnd  14295  swrdswrdlem  14345  swrdswrd  14346  pfxccat3  14375  reuccatpfxs1  14388  repswswrd  14425  repswccat  14427  cshwidxmod  14444  2cshwcshw  14466  s4f1o  14559  wwlktovfo  14601  relexpindlem  14702  resqrex  14890  summo  15357  fsum2d  15411  modfsummods  15433  binom  15470  clim2prod  15528  fprod2d  15619  binomfallfac  15679  efexp  15738  demoivreALT  15838  divconjdvds  15952  addmodlteqALT  15962  dfgcd2  16182  lcmfunsnlem2lem1  16271  lcmfdvdsb  16276  lcmfun  16278  coprmprod  16294  coprmproddvdslem  16295  oddprmdvds  16532  ramcl  16658  prmgaplem6  16685  cshwsidrepswmod0  16724  cshwshashlem1  16725  cshwshashlem2  16726  ressress  16884  initoeu2lem1  17645  symggen  18993  pmtr3ncom  18998  srgmulgass  19682  srgbinom  19696  ringinvnzdiv  19747  lmodvsmmulgdi  20073  psgndiflemB  20717  assamulgscmlem2  21014  mptcoe1fsupp  21296  coe1fzgsumdlem  21382  evl1gsumdlem  21432  scmatmulcl  21575  mdetdiagid  21657  pm2mpf1  21856  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chpdmat  21898  chfacfisf  21911  chfacfisfcpmat  21912  chcoeffeq  21943  topbas  22030  elcls  22132  elcls3  22142  2ndcdisj  22515  filufint  22979  ovoliunlem3  24573  dvge0  25075  ulmcn  25463  gausslemma2dlem3  26421  sizusglecusg  27733  upgriswlk  27910  2pthnloop  28000  crctcshwlkn0  28087  wlknwwlksnbij  28154  wwlksnred  28158  wwlksnext  28159  wwlksnextinj  28165  wwlksnextproplem2  28176  wwlksnextproplem3  28177  usgr2wspthons3  28230  clwwlkccatlem  28254  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  erclwwlktr  28287  clwwlkinwwlk  28305  clwwlkf  28312  clwwlkf1  28314  wwlksext2clwwlk  28322  clwwlknscsh  28327  umgr2cwwk2dif  28329  erclwwlkntr  28336  clwwlknonex2  28374  uhgr3cyclex  28447  upgr4cycl4dv4e  28450  eucrctshift  28508  3cyclfrgrrn1  28550  frgrwopreglem2  28578  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  numclwwlk1lem2fo  28623  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  frgrreg  28659  friendshipgt3  28663  friendship  28664  ipasslem1  29094  shmodsi  29652  elspansn5  29837  h1datomi  29844  nmopsetretALT  30126  pjss2coi  30427  pj3cor1i  30472  mdexchi  30598  atcvat4i  30660  mdsymlem3  30668  mdsymlem4  30669  sumdmdii  30678  cdj3lem2b  30700  elabreximd  30756  iuninc  30801  iundisjf  30829  xrsmulgzz  31189  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  ofldchr  31415  locfinreflem  31692  xrge0iifiso  31787  lmxrge0  31804  esumfzf  31937  sigaclfu2  31989  signstfvneq0  32451  satfrel  33229  satfrnmapom  33232  fmlafvel  33247  fmlasuc  33248  bccolsum  33611  faclimlem1  33615  naddssim  33764  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  segletr  34343  segleantisym  34344  outsideoftr  34358  exp5d  34418  elicc3  34433  finxpreclem2  35488  wl-sbcom2d  35643  poimirlem26  35730  mblfinlem3  35743  itg2addnc  35758  indexa  35818  ax12indalem  36886  ax12inda2ALT  36887  cvrat4  37384  elpaddn0  37741  paddasslem5  37765  paddasslem14  37774  eldioph2  40500  pell1234qrdich  40599  gneispb  41630  rexlimd3  42582  rexabslelem  42848  climsuselem1  43038  stoweidlem19  43450  stoweidlem20  43451  stoweidlem34  43465  wallispilem3  43498  sge0iunmpt  43846  meaiuninc3v  43912  smflimmpt  44230  or2expropbilem1  44413  fsetprcnexALT  44443  2reu8i  44492  2elfz2melfz  44698  subsubelfzo0  44706  iccpartigtl  44763  iccpartgt  44767  icceuelpartlem  44775  fargshiftf1  44781  ich2exprop  44811  ichreuopeq  44813  lighneallem3  44947  gbowgt5  45102  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  isomuspgrlem2b  45169  upgrwlkupwlk  45190  2zrngagrp  45389  rhmsubcrngclem2  45474  nzerooringczr  45518  lmodvsmdi  45606  ply1mulgsumlem1  45615  elfzolborelfzop1  45748  nnolog2flm1  45824  nn0sumshdiglemA  45853  eenglngeehlnmlem2  45972