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

This theorem is referenced by:  exp41  434  exp42  435  imp5a  440  expl  457  anasss  466  an31s  654  exbiri  810  3exp  1119  exp516  1357  rexlimdva2  3136  r19.29af2  3245  reusv2lem2  5354  pwssun  5530  onmindif  6426  mpteqb  6987  dffo3f  7078  fompt  7090  fliftfun  7287  elovmpt3rab1  7649  ordsucss  7793  tfindsg  7837  tfrlem1  8344  tfrlem9  8353  oaordi  8510  oaordex  8522  oaass  8525  oarec  8526  omass  8544  oen0  8550  oeordsuc  8558  nnaordi  8582  omsmolem  8621  naddssim  8649  brinxper  8700  infensuc  9119  suppeqfsuppbi  9330  marypha1lem  9384  hartogs  9497  card2on  9507  tz9.12lem3  9742  infxpenlem  9966  cfcoflem  10225  isf32lem12  10317  zorn2lem6  10454  ondomon  10516  axrepnd  10547  fpwwe2lem11  10594  genpcd  10959  ltexprlem6  10994  axpre-sup  11122  negf1o  11608  recex  11810  uzaddcl  12863  nn01to3  12900  rpnnen1lem5  12940  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  fz0fzelfz0  13595  fz0fzdiffz0  13598  elfzmlbp  13600  difelfzle  13602  fzo1fzo0n0  13676  elincfzoext  13684  ssfzo12bi  13722  elfznelfzo  13733  modaddmodup  13899  modfzo0difsn  13908  fsuppmapnn0fiubex  13957  seqf1o  14008  expcllem  14037  expeq0  14057  mulexp  14066  hashgt12el2  14388  hashimarni  14406  hash2prd  14440  fi1uzind  14472  swrdnd  14619  swrdswrdlem  14669  swrdswrd  14670  pfxccat3  14699  reuccatpfxs1  14712  repswswrd  14749  repswccat  14751  cshwidxmod  14768  2cshwcshw  14791  s4f1o  14884  wwlktovfo  14924  relexpindlem  15029  resqrex  15216  summo  15683  fsum2d  15737  modfsummods  15759  binom  15796  clim2prod  15854  fprod2d  15947  binomfallfac  16007  efexp  16069  demoivreALT  16169  divconjdvds  16285  addmodlteqALT  16295  dfgcd2  16516  lcmfunsnlem2lem1  16608  lcmfdvdsb  16613  lcmfun  16615  coprmprod  16631  coprmproddvdslem  16632  oddprmdvds  16874  ramcl  17000  prmgaplem6  17027  cshwsidrepswmod0  17065  cshwshashlem1  17066  cshwshashlem2  17067  ressress  17217  initoeu2lem1  17976  symggen  19400  pmtr3ncom  19405  srgmulgass  20126  srgbinom  20140  ringinvnzdiv  20210  rhmsubcrngclem2  20576  lmodvsmmulgdi  20803  nzerooringczr  21390  psgndiflemB  21509  assamulgscmlem2  21809  mptcoe1fsupp  22100  coe1fzgsumdlem  22190  evl1gsumdlem  22243  scmatmulcl  22405  mdetdiagid  22487  pm2mpf1  22686  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chpdmat  22728  chfacfisf  22741  chfacfisfcpmat  22742  chcoeffeq  22773  topbas  22859  elcls  22960  elcls3  22970  2ndcdisj  23343  filufint  23807  ovoliunlem3  25405  dvge0  25911  ulmcn  26308  gausslemma2dlem3  27279  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  sizusglecusg  29391  upgriswlk  29569  2pthnloop  29661  crctcshwlkn0  29751  wlknwwlksnbij  29818  wwlksnred  29822  wwlksnext  29823  wwlksnextinj  29829  wwlksnextproplem2  29840  wwlksnextproplem3  29841  usgr2wspthons3  29894  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  erclwwlktr  29951  clwwlkinwwlk  29969  clwwlkf  29976  clwwlkf1  29978  wwlksext2clwwlk  29986  clwwlknscsh  29991  umgr2cwwk2dif  29993  erclwwlkntr  30000  clwwlknonex2  30038  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  eucrctshift  30172  3cyclfrgrrn1  30214  frgrwopreglem2  30242  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  numclwwlk1lem2fo  30287  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  frgrreg  30323  friendshipgt3  30327  friendship  30328  ipasslem1  30760  shmodsi  31318  elspansn5  31503  h1datomi  31510  nmopsetretALT  31792  pjss2coi  32093  pj3cor1i  32138  mdexchi  32264  atcvat4i  32326  mdsymlem3  32334  mdsymlem4  32335  sumdmdii  32344  cdj3lem2b  32366  elabreximd  32439  iuninc  32489  iundisjf  32518  xrsmulgzz  32947  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  ofldchr  33292  unitprodclb  33360  rprmdvdsprod  33505  1arithidom  33508  constrmon  33734  locfinreflem  33830  xrge0iifiso  33925  lmxrge0  33942  esumfzf  34059  sigaclfu2  34111  signstfvneq0  34563  satfrel  35354  satfrnmapom  35357  fmlafvel  35372  fmlasuc  35373  bccolsum  35726  faclimlem1  35730  segletr  36102  segleantisym  36103  outsideoftr  36117  exp5d  36290  elicc3  36305  finxpreclem2  37378  wl-sbcom2d  37549  poimirlem26  37640  mblfinlem3  37653  itg2addnc  37668  indexa  37727  disjlem19  38793  ax12indalem  38938  ax12inda2ALT  38939  cvrat4  39437  elpaddn0  39794  paddasslem5  39818  paddasslem14  39827  eldioph2  42750  pell1234qrdich  42849  oaabsb  43283  onmcl  43320  tfsconcat0b  43335  oaun3lem1  43363  oaun3lem2  43364  naddgeoa  43383  gneispb  44120  rexlimd3  45138  rexabslelem  45414  climsuselem1  45605  stoweidlem19  46017  stoweidlem20  46018  stoweidlem34  46032  wallispilem3  46065  sge0iunmpt  46416  meaiuninc3v  46482  smflimmpt  46808  or2expropbilem1  47033  fsetprcnexALT  47063  2reu8i  47114  2elfz2melfz  47319  subsubelfzo0  47327  iccpartigtl  47424  iccpartgt  47428  icceuelpartlem  47436  fargshiftf1  47442  ich2exprop  47472  ichreuopeq  47474  lighneallem3  47608  gbowgt5  47763  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgblthelfgott  47816  grimco  47889  isuspgrimlem  47895  grimedg  47935  upgrwlkupwlk  48128  2zrngagrp  48237  lmodvsmdi  48367  ply1mulgsumlem1  48375  elfzolborelfzop1  48508  nnolog2flm1  48579  nn0sumshdiglemA  48608  eenglngeehlnmlem2  48727