Theorem exp31 423

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  exp41  438  exp42  439  imp5a  444  expl  461  anasss  470  an31s  654  exbiri  811  3exp  1120  exp516  1357  rexlimdva2  3197  r19.29af2  3239  reusv2lem2  5267  pwssun  5426  onmindif  6262  mpteqb  6795  fliftfun  7079  elovmpt3rab1  7422  ordsucss  7553  tfindsg  7595  tfrlem1  8042  tfrlem9  8051  oaordi  8204  oaordex  8216  oaass  8219  oarec  8220  omass  8238  oen0  8244  oeordsuc  8252  nnaordi  8276  omsmolem  8312  infensuc  8746  php3  8754  suppeqfsuppbi  8921  marypha1lem  8971  hartogs  9082  card2on  9092  tz9.12lem3  9292  infxpenlem  9514  cfcoflem  9773  isf32lem12  9865  zorn2lem6  10002  ondomon  10064  axrepnd  10095  fpwwe2lem11  10142  genpcd  10507  ltexprlem6  10542  axpre-sup  10670  negf1o  11149  recex  11351  uzaddcl  12387  nn01to3  12424  rpnnen1lem5  12464  xrsupsslem  12784  xrinfmsslem  12785  supxrunb1  12796  supxrunb2  12797  fz0fzelfz0  13105  fz0fzdiffz0  13108  elfzmlbp  13110  difelfzle  13112  fzo1fzo0n0  13180  elincfzoext  13187  ssfzo12bi  13224  elfznelfzo  13234  modaddmodup  13394  modfzo0difsn  13403  fsuppmapnn0fiubex  13452  seqf1o  13504  expcllem  13533  expeq0  13552  mulexp  13561  hashgt12el2  13877  hashimarni  13895  hash2prd  13928  fi1uzind  13950  swrdnd  14106  swrdswrdlem  14156  swrdswrd  14157  pfxccat3  14186  reuccatpfxs1  14199  repswswrd  14236  repswccat  14238  cshwidxmod  14255  2cshwcshw  14277  s4f1o  14370  wwlktovfo  14412  relexpindlem  14513  resqrex  14701  summo  15168  fsum2d  15220  modfsummods  15242  binom  15279  clim2prod  15337  fprod2d  15428  binomfallfac  15488  efexp  15547  demoivreALT  15647  divconjdvds  15761  addmodlteqALT  15771  dfgcd2  15991  lcmfunsnlem2lem1  16080  lcmfdvdsb  16085  lcmfun  16087  coprmprod  16103  coprmproddvdslem  16104  oddprmdvds  16340  ramcl  16466  prmgaplem6  16493  cshwsidrepswmod0  16532  cshwshashlem1  16533  cshwshashlem2  16534  ressress  16666  initoeu2lem1  17387  symggen  18717  pmtr3ncom  18722  srgmulgass  19401  srgbinom  19415  ringinvnzdiv  19466  lmodvsmmulgdi  19789  psgndiflemB  20417  assamulgscmlem2  20715  mptcoe1fsupp  20991  coe1fzgsumdlem  21077  evl1gsumdlem  21127  scmatmulcl  21270  mdetdiagid  21352  pm2mpf1  21551  mptcoe1matfsupp  21554  mp2pm2mplem4  21561  chpdmat  21593  chfacfisf  21606  chfacfisfcpmat  21607  chcoeffeq  21638  topbas  21724  elcls  21825  elcls3  21835  2ndcdisj  22208  filufint  22672  ovoliunlem3  24257  dvge0  24758  ulmcn  25146  gausslemma2dlem3  26104  sizusglecusg  27405  upgriswlk  27582  2pthnloop  27672  crctcshwlkn0  27759  wlknwwlksnbij  27826  wwlksnred  27830  wwlksnext  27831  wwlksnextinj  27837  wwlksnextproplem2  27848  wwlksnextproplem3  27849  usgr2wspthons3  27902  clwwlkccatlem  27926  clwlkclwwlklem2a4  27934  clwlkclwwlklem2a  27935  clwlkclwwlklem2  27937  erclwwlktr  27959  clwwlkinwwlk  27977  clwwlkf  27984  clwwlkf1  27986  wwlksext2clwwlk  27994  clwwlknscsh  27999  umgr2cwwk2dif  28001  erclwwlkntr  28008  clwwlknonex2  28046  uhgr3cyclex  28119  upgr4cycl4dv4e  28122  eucrctshift  28180  3cyclfrgrrn1  28222  frgrwopreglem2  28250  frgrwopreglem5  28258  frgrwopreglem5ALT  28259  numclwwlk1lem2fo  28295  numclwlk2lem2f  28314  numclwlk2lem2f1o  28316  frgrreg  28331  friendshipgt3  28335  friendship  28336  ipasslem1  28766  shmodsi  29324  elspansn5  29509  h1datomi  29516  nmopsetretALT  29798  pjss2coi  30099  pj3cor1i  30144  mdexchi  30270  atcvat4i  30332  mdsymlem3  30340  mdsymlem4  30341  sumdmdii  30350  cdj3lem2b  30372  elabreximd  30429  iuninc  30474  iundisjf  30502  xrsmulgzz  30864  gsumle  30927  gsumvsca1  31056  gsumvsca2  31057  ofldchr  31090  locfinreflem  31362  xrge0iifiso  31457  lmxrge0  31474  esumfzf  31607  sigaclfu2  31659  signstfvneq0  32121  satfrel  32900  satfrnmapom  32903  fmlafvel  32918  fmlasuc  32919  bccolsum  33276  faclimlem1  33280  dftrpred3g  33375  naddssim  33478  nosupbnd1  33558  nosupbnd2  33560  noinfbnd1  33573  noinfbnd2  33575  segletr  34054  segleantisym  34055  outsideoftr  34069  exp5d  34129  elicc3  34144  finxpreclem2  35181  wl-sbcom2d  35336  poimirlem26  35423  mblfinlem3  35436  itg2addnc  35451  indexa  35511  ax12indalem  36579  ax12inda2ALT  36580  cvrat4  37077  elpaddn0  37434  paddasslem5  37458  paddasslem14  37467  eldioph2  40148  pell1234qrdich  40247  gneispb  41279  rexlimd3  42223  rexabslelem  42488  climsuselem1  42682  stoweidlem19  43094  stoweidlem20  43095  stoweidlem34  43109  wallispilem3  43142  sge0iunmpt  43490  meaiuninc3v  43556  smflimmpt  43874  or2expropbilem1  44057  fsetprcnexALT  44086  2reu8i  44130  2elfz2melfz  44336  subsubelfzo0  44344  iccpartigtl  44401  iccpartgt  44405  icceuelpartlem  44413  fargshiftf1  44419  ich2exprop  44449  ichreuopeq  44451  lighneallem3  44585  gbowgt5  44740  bgoldbtbndlem3  44785  bgoldbtbndlem4  44786  bgoldbtbnd  44787  tgblthelfgott  44793  isomuspgrlem2b  44807  upgrwlkupwlk  44828  2zrngagrp  45027  rhmsubcrngclem2  45112  nzerooringczr  45156  lmodvsmdi  45244  ply1mulgsumlem1  45253  elfzolborelfzop1  45386  nnolog2flm1  45462  nn0sumshdiglemA  45491  eenglngeehlnmlem2  45610