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  3171  r19.29af2  3276  reusv2lem2  5375  pwssun  5558  onmindif  6462  mpteqb  7016  dffo3f  7108  fompt  7120  fliftfun  7321  elovmpt3rab1  7683  ordsucss  7823  tfindsg  7866  tfrlem1  8371  tfrlem9  8381  oaordi  8540  oaordex  8552  oaass  8555  oarec  8556  omass  8574  oen0  8581  oeordsuc  8589  nnaordi  8613  omsmolem  8652  naddssim  8681  brinxper  8733  infensuc  9153  suppeqfsuppbi  9349  marypha1lem  9403  hartogs  9516  card2on  9526  tz9.12lem3  9771  infxpenlem  10016  cfcoflem  10274  isf32lem12  10366  zorn2lem6  10503  ondomon  10565  axrepnd  10597  fpwwe2lem11  10644  genpcd  11009  ltexprlem6  11044  axpre-sup  11172  negf1o  11662  recex  11864  uzaddcl  12946  nn01to3  12983  rpnnen1lem5  13023  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  supxrunb2  13364  fz0fzelfz0  13681  fz0fzdiffz0  13684  elfzmlbp  13686  difelfzle  13688  fzo1fzo0n0  13763  elincfzoext  13771  ssfzo12bi  13809  elfznelfzo  13821  modaddmodup  13990  modfzo0difsn  13999  fsuppmapnn0fiubex  14048  seqf1o  14099  expcllem  14128  expeq0  14148  mulexp  14157  hashgt12el2  14480  hashimarni  14498  hash2prd  14532  fi1uzind  14564  swrdnd  14716  swrdswrdlem  14765  swrdswrd  14766  pfxccat3  14795  reuccatpfxs1  14808  repswswrd  14847  repswccat  14849  cshwidxmod  14866  2cshwcshw  14888  s4f1o  14981  wwlktovfo  15021  relexpindlem  15126  resqrex  15327  summo  15794  fsum2d  15848  modfsummods  15871  binom  15910  clim2prod  15968  fprod2d  16061  binomfallfac  16120  efexp  16182  demoivreALT  16282  divconjdvds  16398  addmodlteqALT  16408  dfgcd2  16629  lcmfunsnlem2lem1  16721  lcmfdvdsb  16726  lcmfun  16728  coprmprod  16744  coprmproddvdslem  16745  oddprmdvds  16988  ramcl  17114  prmgaplem6  17141  cshwsidrepswmod0  17179  cshwshashlem1  17180  cshwshashlem2  17181  ressress  17332  initoeu2lem1  18096  symggen  19571  pmtr3ncom  19576  gsumle  20246  srgmulgass  20330  srgbinom  20344  ringinvnzdiv  20417  rhmsubcrngclem2  20803  lmodvsmmulgdi  21055  nzerooringczr  21667  ofldchr  21763  psgndiflemB  21787  assamulgscmlem2  22087  mptcoe1fsupp  22412  coe1fzgsumdlem  22500  evl1gsumdlem  22553  scmatmulcl  22712  mdetdiagid  22794  pm2mpf1  22993  mptcoe1matfsupp  22996  mp2pm2mplem4  23003  chpdmat  23035  chfacfisf  23048  chfacfisfcpmat  23049  chcoeffeq  23080  topbas  23166  elcls  23267  elcls3  23277  2ndcdisj  23650  filufint  24114  ovoliunlem3  25700  dvge0  26202  ulmcn  26599  gausslemma2dlem3  27569  nosupbnd1  27915  nosupbnd2  27917  noinfbnd1  27930  noinfbnd2  27932  sizusglecusg  29850  upgriswlk  30027  2pthnloop  30117  crctcshwlkn0  30207  wlknwwlksnbij  30274  wwlksnred  30278  wwlksnext  30279  wwlksnextinj  30285  wwlksnextproplem2  30296  wwlksnextproplem3  30297  usgr2wspthons3  30353  clwwlkccatlem  30377  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  erclwwlktr  30410  clwwlkinwwlk  30428  clwwlkf  30435  clwwlkf1  30437  wwlksext2clwwlk  30445  clwwlknscsh  30450  umgr2cwwk2dif  30452  erclwwlkntr  30459  clwwlknonex2  30497  uhgr3cyclex  30570  upgr4cycl4dv4e  30573  eucrctshift  30631  3cyclfrgrrn1  30673  frgrwopreglem2  30701  frgrwopreglem5  30709  frgrwopreglem5ALT  30710  numclwwlk1lem2fo  30746  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  frgrreg  30782  friendshipgt3  30786  friendship  30787  ipasslem1  31220  shmodsi  31778  elspansn5  31963  h1datomi  31970  nmopsetretALT  32252  pjss2coi  32553  pj3cor1i  32598  mdexchi  32724  atcvat4i  32786  mdsymlem3  32794  mdsymlem4  32795  sumdmdii  32804  cdj3lem2b  32826  elabreximd  32893  iuninc  32942  iundisjf  32971  xrsmulgzz  33360  gsumvsca1  33577  gsumvsca2  33578  unitprodclb  33733  rprmdvdsprod  33855  1arithidom  33858  constrmon  34165  locfinreflem  34261  xrge0iifiso  34356  lmxrge0  34373  esumfzf  34490  sigaclfu2  34542  signstfvneq0  34991  satfrel  35880  satfrnmapom  35883  fmlafvel  35898  fmlasuc  35899  bccolsum  36252  faclimlem1  36256  segletr  36627  segleantisym  36628  outsideoftr  36642  exp5d  36855  elicc3  36869  finxpreclem2  38077  wl-sbcom2d  38257  poimirlem26  38338  mblfinlem3  38351  itg2addnc  38366  indexa  38425  disjlem19  39594  ax12indalem  39760  ax12inda2ALT  39761  cvrat4  40258  elpaddn0  40615  paddasslem5  40639  paddasslem14  40648  eldioph2  43534  pell1234qrdich  43629  oaabsb  44062  onmcl  44099  tfsconcat0b  44114  oaun3lem1  44142  oaun3lem2  44143  naddgeoa  44162  gneispb  44898  rexlimd3  45903  rexabslelem  46173  climsuselem1  46364  stoweidlem19  46774  stoweidlem20  46775  stoweidlem34  46789  wallispilem3  46822  sge0iunmpt  47173  meaiuninc3v  47239  smflimmpt  47565  or2expropbilem1  47810  fsetprcnexALT  47840  2reu8i  47891  2elfz2melfz  48096  subsubelfzo0  48105  iccpartigtl  48213  iccpartgt  48217  icceuelpartlem  48225  fargshiftf1  48231  ich2exprop  48261  ichreuopeq  48263  lighneallem3  48400  gbowgt5  48568  bgoldbtbndlem3  48613  bgoldbtbndlem4  48614  bgoldbtbnd  48615  tgblthelfgott  48621  grimco  48695  isuspgrimlem  48701  grimedg  48741  upgrwlkupwlk  48946  2zrngagrp  49055  lmodvsmdi  49200  ply1mulgsumlem1  49207  elfzolborelfzop1  49340  nnolog2flm1  49411  nn0sumshdiglemA  49440  eenglngeehlnmlem2  49559