Theorem exp31 425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp41  440  exp42  441  imp5a  446  expl  463  anasss  472  an31s  667  exbiri  823  3exp  1137  exp516  1375  rexlimdva2  3169  r19.29af2  3274  reusv2lem2  5366  pwssun  5548  onmindif  6478  mpteqb  7039  dffo3f  7133  fompt  7145  fliftfun  7346  elovmpt3rab1  7708  ordsucss  7856  tfindsg  7899  tfrlem1  8414  tfrlem9  8424  oaordi  8585  oaordex  8597  oaass  8600  oarec  8601  omass  8619  oen0  8626  oeordsuc  8634  nnaordi  8658  omsmolem  8697  naddssim  8726  brinxper  8778  infensuc  9205  suppeqfsuppbi  9401  marypha1lem  9455  hartogs  9568  card2on  9578  tz9.12lem3  9826  infxpenlem  10122  cfcoflem  10380  isf32lem12  10472  zorn2lem6  10609  ondomon  10677  axrepnd  10709  fpwwe2lem11  10756  genpcd  11121  ltexprlem6  11156  axpre-sup  11284  negf1o  11776  recex  11978  uzaddcl  13061  nn01to3  13098  rpnnen1lem5  13139  xrsupsslem  13467  xrinfmsslem  13468  supxrunb1  13479  supxrunb2  13480  fz0fzelfz0  13798  fz0fzdiffz0  13801  elfzmlbp  13803  difelfzle  13805  fzo1fzo0n0  13880  elincfzoext  13888  ssfzo12bi  13926  elfznelfzo  13938  modaddmodup  14107  modfzo0difsn  14116  fsuppmapnn0fiubex  14165  seqf1o  14216  expcllem  14245  expeq0  14265  mulexp  14274  hashgt12el2  14598  hashimarni  14616  hash2prd  14650  fi1uzind  14682  swrdnd  14835  swrdswrdlem  14884  swrdswrd  14885  pfxccat3  14914  reuccatpfxs1  14927  repswswrd  14966  repswccat  14968  cshwidxmod  14985  2cshwcshw  15007  s4f1o  15101  wwlktovfo  15143  relexpindlem  15248  resqrex  15449  summo  15915  fsum2d  15969  modfsummods  15992  binom  16031  clim2prod  16089  fprod2d  16180  binomfallfac  16239  efexp  16301  demoivreALT  16401  divconjdvds  16517  addmodlteqALT  16527  dfgcd2  16751  lcmfunsnlem2lem1  16845  lcmfdvdsb  16850  lcmfun  16852  coprmprod  16868  coprmproddvdslem  16869  oddprmdvds  17113  ramcl  17239  prmgaplem6  17266  cshwsidrepswmod0  17304  cshwshashlem1  17305  cshwshashlem2  17306  ressress  17457  initoeu2lem1  18221  mgmn0plusgplusf  18860  symggen  19717  pmtr3ncom  19722  gsumle  20392  srgmulgass  20476  srgbinom  20490  ringinvnzdiv  20565  rhmsubcrngclem2  20952  lmodvsmmulgdi  21205  nzerooringczr  21819  ofldchr  21915  psgndiflemB  21939  assamulgscmlem2  22241  mptcoe1fsupp  22566  coe1fzgsumdlem  22654  evl1gsumdlem  22707  scmatmulcl  22866  mdetdiagid  22948  pm2mpf1  23150  mptcoe1matfsupp  23153  mp2pm2mplem4  23160  chpdmat  23192  chfacfisf  23205  chfacfisfcpmat  23206  chcoeffeq  23237  topbas  23323  elcls  23424  elcls3  23434  2ndcdisj  23808  filufint  24272  ovoliunlem3  25858  dvge0  26359  ulmcn  26759  gausslemma2dlem3  27728  nosupbnd1  28104  nosupbnd2  28106  noinfbnd1  28119  noinfbnd2  28121  sizusglecusg  30077  upgriswlk  30254  2pthnloop  30350  crctcshwlkn0  30443  wlknwwlksnbij  30510  wwlksnred  30514  wwlksnext  30515  wwlksnextinj  30521  wwlksnextproplem2  30532  wwlksnextproplem3  30533  usgr2wspthons3  30589  clwwlkccatlem  30613  clwlkclwwlklem2a4  30621  clwlkclwwlklem2a  30622  clwlkclwwlklem2  30624  erclwwlktr  30646  clwwlkinwwlk  30664  clwwlkf  30671  clwwlkf1  30673  wwlksext2clwwlk  30681  clwwlknscsh  30686  umgr2cwwk2dif  30688  erclwwlkntr  30695  clwwlknonex2  30733  uhgr3cyclex  30816  upgr4cycl4dv4e  30819  eucrctshift  30877  3cyclfrgrrn1  30919  frgrwopreglem2  30947  frgrwopreglem5  30955  frgrwopreglem5ALT  30956  numclwwlk1lem2fo  30992  numclwlk2lem2f  31011  numclwlk2lem2f1o  31013  frgrreg  31028  friendshipgt3  31032  friendship  31033  ipasslem1  31466  shmodsi  32024  elspansn5  32209  h1datomi  32216  nmopsetretALT  32498  pjss2coi  32799  pj3cor1i  32844  mdexchi  32970  atcvat4i  33032  mdsymlem3  33040  mdsymlem4  33041  sumdmdii  33050  cdj3lem2b  33072  elabreximd  33181  iuninc  33230  iundisjf  33258  acunirnmpt2  33329  acunirnmpt2f  33330  xrsmulgzz  33646  gsumvsca1  33863  gsumvsca2  33864  unitprodclb  34028  rprmdvdsprod  34150  1arithidom  34153  constrmon  34459  locfinreflem  34555  xrge0iifiso  34650  lmxrge0  34667  esumfzf  34784  sigaclfu2  34836  signstfvneq0  35284  satfrel  36312  satfrnmapom  36315  fmlafvel  36330  fmlasuc  36331  bccolsum  36695  faclimlem1  36699  segletr  37070  segleantisym  37071  outsideoftr  37085  exp5d  37282  elicc3  37296  mh-inf3f1  37520  finxpreclem2  38518  wl-sbcom2d  38698  poimirlem26  38769  mblfinlem3  38782  itg2addnc  38797  indexa  38872  disjlem19  40039  ax12indalem  40205  ax12inda2ALT  40206  cvrat4  40703  elpaddn0  41060  paddasslem5  41084  paddasslem14  41093  eldioph2  43977  pell1234qrdich  44072  oaabsb  44499  onmcl  44536  tfsconcat0b  44551  oaun3lem1  44579  oaun3lem2  44580  naddgeoa  44599  gneispb  45334  rexlimd3  46374  rexabslelem  46643  climsuselem1  46834  stoweidlem19  47244  stoweidlem20  47245  stoweidlem34  47259  wallispilem3  47292  sge0iunmpt  47643  meaiuninc3v  47709  smflimmpt  48035  or2expropbilem1  48317  fsetprcnexALT  48347  2reu8i  48399  2elfz2melfz  48603  subsubelfzo0  48612  iccpartigtl  48720  iccpartgt  48724  icceuelpartlem  48732  fargshiftf1  48738  ich2exprop  48768  ichreuopeq  48770  lighneallem3  48907  gbowgt5  49075  bgoldbtbndlem3  49120  bgoldbtbndlem4  49121  bgoldbtbnd  49122  tgblthelfgott  49128  grimco  49202  isuspgrimlem  49208  grimedg  49248  upgrwlkupwlk  49453  2zrngagrp  49561  lmodvsmdi  49706  ply1mulgsumlem1  49713  elfzolborelfzop1  49846  nnolog2flm1  49917  nn0sumshdiglemA  49946  eenglngeehlnmlem2  50066