Theorem exp31 628

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  exp41  636  exp42  637  expl  646  exbiri  650  anasss  677  an31s  844  pm3.2an3  1233  3impa  1251  exp516  1279  r19.29af2  3057  reusv2lem2  4795  pwssun  4944  onmindif  5732  mpteqb  6207  dffo3  6282  fliftfun  6462  elovmpt3rab1  6791  ordsucss  6910  tfindsg  6952  imacosupp  7222  tfrlem1  7359  tfrlem9  7368  oaordi  7513  oaordex  7525  oaass  7528  oarec  7529  omlimcl  7545  omass  7547  oen0  7553  oeordsuc  7561  nnaordi  7585  omsmolem  7620  infensuc  8023  php3  8031  marypha1lem  8222  hartogs  8332  card2on  8342  tz9.12lem3  8535  infxpenlem  8719  cfflb  8964  cfcoflem  8977  cfcof  8979  isf32lem12  9069  zorn2lem6  9206  ondomon  9264  alephval2  9273  pwcfsdom  9284  axrepnd  9295  fpwwe2lem12  9342  genpcd  9707  ltexprlem6  9742  recexsr  9807  axpre-sup  9869  negf1o  10339  recex  10538  zdiv  11323  uzaddcl  11620  nn01to3  11657  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  fz0fzelfz0  12314  fz0fzdiffz0  12317  elfzmlbp  12319  difelfzle  12321  fzo1fzo0n0  12386  elincfzoext  12393  ssfzo12bi  12429  elfznelfzo  12439  modaddmodup  12595  modfzo0difsn  12604  fsuppmapnn0fiubex  12654  seqf1o  12704  expcllem  12733  expeq0  12752  mulexp  12761  hashgt12el2  13071  hashimarni  13086  hash2prd  13114  fi1uzind  13134  fi1uzindOLD  13140  swrdnd  13284  swrdswrdlem  13311  swrdswrd  13312  swrdccat3  13343  swrdccatid  13348  repswswrd  13382  repswccat  13383  cshwidxmod  13400  2cshwcshw  13422  s4f1o  13513  wwlktovfo  13549  cjexp  13738  resqrex  13839  absexp  13892  summo  14295  fsum2d  14344  modfsummods  14366  binom  14401  clim2prod  14459  fprod2d  14550  binomfallfac  14611  efexp  14670  demoivreALT  14770  divconjdvds  14875  addmodlteqALT  14885  dfgcd2  15101  lcmfunsnlem2lem1  15189  lcmfdvdsb  15194  lcmfun  15196  coprmprod  15213  coprmproddvdslem  15214  oddprmdvds  15445  ramcl  15571  cshwsidrepswmod0  15639  cshwshashlem1  15640  ressress  15765  initoeu2lem1  16487  symggen  17713  pmtr3ncom  17718  srgmulgass  18354  srgbinom  18368  ringinvnzdiv  18416  lmodvsmmulgdi  18721  assamulgscmlem2  19170  mptcoe1fsupp  19406  coe1fzgsumdlem  19492  evl1gsumdlem  19541  psgndiflemB  19765  scmatmulcl  20143  mdetdiagid  20225  pm2mpf1  20423  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chpdmat  20465  chfacfisf  20478  chfacfisfcpmat  20479  chcoeffeq  20510  topbas  20587  fctop  20618  cctop  20620  elcls  20687  elcls3  20697  2ndcdisj  21069  filufint  21534  ovoliunlem3  23079  dvge0  23573  ulmcn  23957  gausslemma2dlem3  24893  usgrares1  25939  cusgrarn  25988  cusgrares  26001  usgrasscusgra  26011  pthdepisspth  26104  usgra2adedgspthlem2  26140  usgra2wlkspthlem1  26147  usgra2wlkspth  26149  fargshiftf1  26165  usgrcyclnl2  26169  constr3trllem2  26179  wlkiswwlk1  26218  wwlknred  26251  wwlkextinj  26258  wwlkextproplem2  26270  0clwlk  26293  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkf  26322  clwwlkf1  26324  wwlkext2clwwlk  26331  clwwisshclww  26335  erclwwlktr  26343  clwwlknscsh  26347  usg2cwwk2dif  26348  erclwwlkntr  26355  clwlkfclwwlk  26371  clwlkf1clwwlklem  26376  usg2wotspth  26411  usgfidegfi  26437  usgravd00  26446  eupatrl  26495  2pthfrgra  26538  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  frgrancvvdeq  26569  frgrancvvdgeq  26570  frgrawopreglem5  26575  usg2spot2nb  26592  extwwlkfablem1  26601  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  frgrareggt1  26643  frgrareg  26644  friendshipgt3  26648  friendship  26649  grpoinvf  26770  nmosetre  27003  ipasslem1  27070  shmodsi  27632  elspansn5  27817  normcan  27819  h1datomi  27824  nmopsetretALT  28106  nmfnsetre  28120  pjss2coi  28407  pj3cor1i  28452  mdexchi  28578  superpos  28597  atcvat4i  28640  mdsymlem3  28648  mdsymlem4  28649  sumdmdii  28658  cdj3lem2b  28680  elabreximd  28732  iuninc  28761  iundisjf  28784  xrsmulgzz  29009  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  ofldchr  29145  locfinreflem  29235  xrge0iifiso  29309  lmxrge0  29326  esumfzf  29458  sigaclfu2  29511  eulerpartlemgh  29767  signstfvneq0  29975  signstfvc  29977  bccolsum  30878  faclimlem1  30882  dftrpred3g  30977  segletr  31391  segleantisym  31392  outsideoftr  31406  exp5d  31466  elicc3  31481  finxpreclem2  32403  wl-sbcom2d  32523  poimirlem26  32605  mblfinlem3  32618  itg2addnc  32634  indexa  32698  ax12indalem  33248  ax12inda2ALT  33249  cvrat4  33747  elpaddn0  34104  paddasslem5  34128  paddasslem14  34137  eldioph2  36343  pell1234qrdich  36443  gneispb  37449  dffo3f  38359  climsuselem1  38674  stoweidlem19  38912  stoweidlem20  38913  stoweidlem34  38927  wallispilem3  38960  sge0iunmpt  39311  smflimlem4  39660  iccpartigtl  39961  iccpartgt  39965  icceuelpartlem  39973  lighneallem3  40062  gbogt5  40184  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgblthelfgott  40229  tgblthelfgottOLD  40236  pfxccat3  40289  2elfz2melfz  40355  subsubelfzo0  40359  sizusglecusg  40679  upgr1wlkwlk  40847  2pthnloop  40937  crctcsh1wlkn0  41024  wwlksnred  41098  wwlksnextinj  41105  wwlksnextproplem2  41116  wwlksnextproplem3  41117  wwlks2onv  41158  usgr2wspthons3  41167  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksf  41222  clwwlksf1  41224  wwlksext2clwwlk  41231  erclwwlkstr  41243  clwwlksnscsh  41247  umgr2cwwk2dif  41248  erclwwlksntr  41255  clwlksfclwwlk  41269  clwlksf1clwwlklem  41275  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  eucrctshift  41411  3cyclfrgrrn1  41455  frgrncvvdeqlemC  41478  frgrwopreglem5  41485  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-frgrareg  41548  av-friendshipgt3  41552  av-friendship  41553  2zrngagrp  41733  rhmsubcrngclem2  41820  nzerooringczr  41864  lmodvsmdi  41957  ply1mulgsumlem1  41968  islindeps2  42066  elfzolborelfzop1  42103  nnolog2flm1  42182  nn0sumshdiglemA  42211