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  3137  r19.29af2  3246  reusv2lem2  5357  pwssun  5533  onmindif  6429  mpteqb  6990  dffo3f  7081  fompt  7093  fliftfun  7290  elovmpt3rab1  7652  ordsucss  7796  tfindsg  7840  tfrlem1  8347  tfrlem9  8356  oaordi  8513  oaordex  8525  oaass  8528  oarec  8529  omass  8547  oen0  8553  oeordsuc  8561  nnaordi  8585  omsmolem  8624  naddssim  8652  brinxper  8703  infensuc  9125  suppeqfsuppbi  9337  marypha1lem  9391  hartogs  9504  card2on  9514  tz9.12lem3  9749  infxpenlem  9973  cfcoflem  10232  isf32lem12  10324  zorn2lem6  10461  ondomon  10523  axrepnd  10554  fpwwe2lem11  10601  genpcd  10966  ltexprlem6  11001  axpre-sup  11129  negf1o  11615  recex  11817  uzaddcl  12870  nn01to3  12907  rpnnen1lem5  12947  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  fz0fzelfz0  13602  fz0fzdiffz0  13605  elfzmlbp  13607  difelfzle  13609  fzo1fzo0n0  13683  elincfzoext  13691  ssfzo12bi  13729  elfznelfzo  13740  modaddmodup  13906  modfzo0difsn  13915  fsuppmapnn0fiubex  13964  seqf1o  14015  expcllem  14044  expeq0  14064  mulexp  14073  hashgt12el2  14395  hashimarni  14413  hash2prd  14447  fi1uzind  14479  swrdnd  14626  swrdswrdlem  14676  swrdswrd  14677  pfxccat3  14706  reuccatpfxs1  14719  repswswrd  14756  repswccat  14758  cshwidxmod  14775  2cshwcshw  14798  s4f1o  14891  wwlktovfo  14931  relexpindlem  15036  resqrex  15223  summo  15690  fsum2d  15744  modfsummods  15766  binom  15803  clim2prod  15861  fprod2d  15954  binomfallfac  16014  efexp  16076  demoivreALT  16176  divconjdvds  16292  addmodlteqALT  16302  dfgcd2  16523  lcmfunsnlem2lem1  16615  lcmfdvdsb  16620  lcmfun  16622  coprmprod  16638  coprmproddvdslem  16639  oddprmdvds  16881  ramcl  17007  prmgaplem6  17034  cshwsidrepswmod0  17072  cshwshashlem1  17073  cshwshashlem2  17074  ressress  17224  initoeu2lem1  17983  symggen  19407  pmtr3ncom  19412  srgmulgass  20133  srgbinom  20147  ringinvnzdiv  20217  rhmsubcrngclem2  20583  lmodvsmmulgdi  20810  nzerooringczr  21397  psgndiflemB  21516  assamulgscmlem2  21816  mptcoe1fsupp  22107  coe1fzgsumdlem  22197  evl1gsumdlem  22250  scmatmulcl  22412  mdetdiagid  22494  pm2mpf1  22693  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  chpdmat  22735  chfacfisf  22748  chfacfisfcpmat  22749  chcoeffeq  22780  topbas  22866  elcls  22967  elcls3  22977  2ndcdisj  23350  filufint  23814  ovoliunlem3  25412  dvge0  25918  ulmcn  26315  gausslemma2dlem3  27286  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2  27650  sizusglecusg  29398  upgriswlk  29576  2pthnloop  29668  crctcshwlkn0  29758  wlknwwlksnbij  29825  wwlksnred  29829  wwlksnext  29830  wwlksnextinj  29836  wwlksnextproplem2  29847  wwlksnextproplem3  29848  usgr2wspthons3  29901  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  erclwwlktr  29958  clwwlkinwwlk  29976  clwwlkf  29983  clwwlkf1  29985  wwlksext2clwwlk  29993  clwwlknscsh  29998  umgr2cwwk2dif  30000  erclwwlkntr  30007  clwwlknonex2  30045  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  eucrctshift  30179  3cyclfrgrrn1  30221  frgrwopreglem2  30249  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  numclwwlk1lem2fo  30294  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  frgrreg  30330  friendshipgt3  30334  friendship  30335  ipasslem1  30767  shmodsi  31325  elspansn5  31510  h1datomi  31517  nmopsetretALT  31799  pjss2coi  32100  pj3cor1i  32145  mdexchi  32271  atcvat4i  32333  mdsymlem3  32341  mdsymlem4  32342  sumdmdii  32351  cdj3lem2b  32373  elabreximd  32446  iuninc  32496  iundisjf  32525  xrsmulgzz  32954  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  ofldchr  33299  unitprodclb  33367  rprmdvdsprod  33512  1arithidom  33515  constrmon  33741  locfinreflem  33837  xrge0iifiso  33932  lmxrge0  33949  esumfzf  34066  sigaclfu2  34118  signstfvneq0  34570  satfrel  35361  satfrnmapom  35364  fmlafvel  35379  fmlasuc  35380  bccolsum  35733  faclimlem1  35737  segletr  36109  segleantisym  36110  outsideoftr  36124  exp5d  36297  elicc3  36312  finxpreclem2  37385  wl-sbcom2d  37556  poimirlem26  37647  mblfinlem3  37660  itg2addnc  37675  indexa  37734  disjlem19  38800  ax12indalem  38945  ax12inda2ALT  38946  cvrat4  39444  elpaddn0  39801  paddasslem5  39825  paddasslem14  39834  eldioph2  42757  pell1234qrdich  42856  oaabsb  43290  onmcl  43327  tfsconcat0b  43342  oaun3lem1  43370  oaun3lem2  43371  naddgeoa  43390  gneispb  44127  rexlimd3  45145  rexabslelem  45421  climsuselem1  45612  stoweidlem19  46024  stoweidlem20  46025  stoweidlem34  46039  wallispilem3  46072  sge0iunmpt  46423  meaiuninc3v  46489  smflimmpt  46815  or2expropbilem1  47037  fsetprcnexALT  47067  2reu8i  47118  2elfz2melfz  47323  subsubelfzo0  47331  iccpartigtl  47428  iccpartgt  47432  icceuelpartlem  47440  fargshiftf1  47446  ich2exprop  47476  ichreuopeq  47478  lighneallem3  47612  gbowgt5  47767  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgblthelfgott  47820  grimco  47893  isuspgrimlem  47899  grimedg  47939  upgrwlkupwlk  48132  2zrngagrp  48241  lmodvsmdi  48371  ply1mulgsumlem1  48379  elfzolborelfzop1  48512  nnolog2flm1  48583  nn0sumshdiglemA  48612  eenglngeehlnmlem2  48731