Theorem exp31 630

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  exp41  638  exp42  639  expl  648  exbiri  652  anasss  679  an31s  848  pm3.2an3  1240  3impa  1259  exp516  1287  r19.29af2  3075  reusv2lem2  4869  pwssun  5020  onmindif  5815  mpteqb  6299  dffo3  6374  fliftfun  6562  elovmpt3rab1  6893  ordsucss  7018  tfindsg  7060  imacosupp  7335  tfrlem1  7472  tfrlem9  7481  oaordi  7626  oaordex  7638  oaass  7641  oarec  7642  omlimcl  7658  omass  7660  oen0  7666  oeordsuc  7674  nnaordi  7698  omsmolem  7733  infensuc  8138  php3  8146  suppeqfsuppbi  8289  marypha1lem  8339  hartogs  8449  card2on  8459  tz9.12lem3  8652  infxpenlem  8836  cfflb  9081  cfcoflem  9094  cfcof  9096  isf32lem12  9186  zorn2lem6  9323  ondomon  9385  alephval2  9394  pwcfsdom  9405  axrepnd  9416  fpwwe2lem12  9463  genpcd  9828  ltexprlem6  9863  recexsr  9928  axpre-sup  9990  negf1o  10460  recex  10659  zdiv  11447  uzaddcl  11744  nn01to3  11781  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  fz0fzelfz0  12445  fz0fzdiffz0  12448  elfzmlbp  12450  difelfzle  12452  fzo1fzo0n0  12518  elincfzoext  12525  ssfzo12bi  12563  elfznelfzo  12573  modaddmodup  12733  modfzo0difsn  12742  fsuppmapnn0fiubex  12792  seqf1o  12842  expcllem  12871  expeq0  12890  mulexp  12899  hashgt12el2  13211  hashimarni  13228  hash2prd  13257  fi1uzind  13279  fi1uzindOLD  13285  swrdnd  13432  swrdswrdlem  13459  swrdswrd  13460  reuccats1  13480  swrdccat3  13492  swrdccatid  13497  repswswrd  13531  repswccat  13532  cshwidxmod  13549  2cshwcshw  13571  s4f1o  13663  wwlktovfo  13701  cjexp  13890  resqrex  13991  absexp  14044  summo  14448  fsum2d  14502  modfsummods  14525  binom  14562  clim2prod  14620  fprod2d  14711  binomfallfac  14772  efexp  14831  demoivreALT  14931  divconjdvds  15037  addmodlteqALT  15047  dfgcd2  15263  lcmfunsnlem2lem1  15351  lcmfdvdsb  15356  lcmfun  15358  coprmprod  15375  coprmproddvdslem  15376  oddprmdvds  15607  ramcl  15733  cshwsidrepswmod0  15801  cshwshashlem1  15802  ressress  15938  initoeu2lem1  16664  symggen  17890  pmtr3ncom  17895  srgmulgass  18531  srgbinom  18545  ringinvnzdiv  18593  lmodvsmmulgdi  18898  assamulgscmlem2  19349  mptcoe1fsupp  19585  coe1fzgsumdlem  19671  evl1gsumdlem  19720  psgndiflemB  19946  scmatmulcl  20324  mdetdiagid  20406  pm2mpf1  20604  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  chpdmat  20646  chfacfisf  20659  chfacfisfcpmat  20660  chcoeffeq  20691  topbas  20776  fctop  20808  cctop  20810  elcls  20877  elcls3  20887  2ndcdisj  21259  filufint  21724  ovoliunlem3  23272  dvge0  23769  ulmcn  24153  gausslemma2dlem3  25093  sizusglecusg  26359  upgriswlk  26537  2pthnloop  26627  crctcshwlkn0  26713  wwlksnred  26787  wwlksnextinj  26794  wwlksnextproplem2  26805  wwlksnextproplem3  26806  wwlks2onv  26847  usgr2wspthons3  26857  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlkinwwlk  26905  clwwlksf  26915  clwwlksf1  26917  wwlksext2clwwlk  26924  erclwwlkstr  26936  clwwlksnscsh  26940  umgr2cwwk2dif  26941  erclwwlksntr  26948  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  eucrctshift  27103  3cyclfrgrrn1  27149  frgrwopreglem2  27177  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  numclwwlkovf2ex  27219  numclwlk1lem2foa  27224  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  frgrreg  27252  friendshipgt3  27256  friendship  27257  grpoinvf  27386  nmosetre  27619  ipasslem1  27686  shmodsi  28248  elspansn5  28433  normcan  28435  h1datomi  28440  nmopsetretALT  28722  nmfnsetre  28736  pjss2coi  29023  pj3cor1i  29068  mdexchi  29194  superpos  29213  atcvat4i  29256  mdsymlem3  29264  mdsymlem4  29265  sumdmdii  29274  cdj3lem2b  29296  elabreximd  29348  iuninc  29379  iundisjf  29402  xrsmulgzz  29678  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  ofldchr  29814  locfinreflem  29907  xrge0iifiso  29981  lmxrge0  29998  esumfzf  30131  sigaclfu2  30184  eulerpartlemgh  30440  signstfvneq0  30649  signstfvc  30651  bccolsum  31625  faclimlem1  31629  dftrpred3g  31733  nosupbnd1  31860  nosupbnd2  31862  segletr  32221  segleantisym  32222  outsideoftr  32236  exp5d  32296  elicc3  32311  finxpreclem2  33227  wl-sbcom2d  33344  poimirlem26  33435  mblfinlem3  33448  itg2addnc  33464  indexa  33528  ax12indalem  34230  ax12inda2ALT  34231  cvrat4  34729  elpaddn0  35086  paddasslem5  35110  paddasslem14  35119  eldioph2  37325  pell1234qrdich  37425  gneispb  38429  rexlimd3  39335  rexlimdva2  39339  dffo3f  39364  rnmptlb  39453  rexabslelem  39645  climsuselem1  39839  limsupubuz  39945  stoweidlem19  40236  stoweidlem20  40237  stoweidlem34  40251  wallispilem3  40284  sge0iunmpt  40635  smflimlem4  40982  smflimmpt  41016  2elfz2melfz  41328  subsubelfzo0  41336  iccpartigtl  41359  iccpartgt  41363  icceuelpartlem  41371  fargshiftf1  41377  pfxccat3  41426  lighneallem3  41524  gbowgt5  41650  mogoldbb  41673  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgblthelfgott  41703  tgblthelfgottOLD  41709  upgrwlkupwlk  41721  2zrngagrp  41943  rhmsubcrngclem2  42028  nzerooringczr  42072  lmodvsmdi  42163  ply1mulgsumlem1  42174  islindeps2  42272  elfzolborelfzop1  42309  nnolog2flm1  42384  nn0sumshdiglemA  42413