Theorem exp31 422

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp41  437  exp42  438  imp5a  443  expl  460  anasss  469  an31s  652  exbiri  809  3exp  1115  exp516  1352  rexlimdva2  3287  r19.29af2  3330  reusv2lem2  5291  pwssun  5449  onmindif  6274  mpteqb  6781  fliftfun  7059  elovmpt3rab1  7399  ordsucss  7527  tfindsg  7569  imacosuppOLD  7869  tfrlem1  8006  tfrlem9  8015  oaordi  8166  oaordex  8178  oaass  8181  oarec  8182  omass  8200  oen0  8206  oeordsuc  8214  nnaordi  8238  omsmolem  8274  infensuc  8689  php3  8697  suppeqfsuppbi  8841  marypha1lem  8891  hartogs  9002  card2on  9012  tz9.12lem3  9212  infxpenlem  9433  cfcoflem  9688  isf32lem12  9780  zorn2lem6  9917  ondomon  9979  axrepnd  10010  fpwwe2lem12  10057  genpcd  10422  ltexprlem6  10457  axpre-sup  10585  negf1o  11064  recex  11266  fiminreOLD  11584  uzaddcl  12298  nn01to3  12335  rpnnen1lem5  12374  xrsupsslem  12694  xrinfmsslem  12695  supxrunb1  12706  supxrunb2  12707  fz0fzelfz0  13007  fz0fzdiffz0  13010  elfzmlbp  13012  difelfzle  13014  fzo1fzo0n0  13082  elincfzoext  13089  ssfzo12bi  13126  elfznelfzo  13136  modaddmodup  13296  modfzo0difsn  13305  fsuppmapnn0fiubex  13354  seqf1o  13405  expcllem  13434  expeq0  13453  mulexp  13462  hashgt12el2  13778  hashimarni  13796  hash2prd  13827  fi1uzind  13849  swrdnd  14010  swrdswrdlem  14060  swrdswrd  14061  pfxccat3  14090  reuccatpfxs1  14103  repswswrd  14140  repswccat  14142  cshwidxmod  14159  2cshwcshw  14181  s4f1o  14274  wwlktovfo  14316  resqrex  14604  summo  15068  fsum2d  15120  modfsummods  15142  binom  15179  clim2prod  15238  fprod2d  15329  binomfallfac  15389  efexp  15448  demoivreALT  15548  divconjdvds  15659  addmodlteqALT  15669  dfgcd2  15888  lcmfunsnlem2lem1  15976  lcmfdvdsb  15981  lcmfun  15983  coprmprod  15999  coprmproddvdslem  16000  oddprmdvds  16233  ramcl  16359  prmgaplem6  16386  cshwsidrepswmod0  16422  cshwshashlem1  16423  cshwshashlem2  16424  ressress  16556  initoeu2lem1  17268  symggen  18592  pmtr3ncom  18597  srgmulgass  19275  srgbinom  19289  ringinvnzdiv  19337  lmodvsmmulgdi  19663  assamulgscmlem2  20123  mptcoe1fsupp  20377  coe1fzgsumdlem  20463  evl1gsumdlem  20513  psgndiflemB  20738  scmatmulcl  21121  mdetdiagid  21203  pm2mpf1  21401  mptcoe1matfsupp  21404  mp2pm2mplem4  21411  chpdmat  21443  chfacfisf  21456  chfacfisfcpmat  21457  chcoeffeq  21488  topbas  21574  elcls  21675  elcls3  21685  2ndcdisj  22058  filufint  22522  ovoliunlem3  24099  dvge0  24597  ulmcn  24981  gausslemma2dlem3  25938  sizusglecusg  27239  upgriswlk  27416  2pthnloop  27506  crctcshwlkn0  27593  wlknwwlksnbij  27660  wwlksnred  27664  wwlksnext  27665  wwlksnextinj  27671  wwlksnextproplem2  27683  wwlksnextproplem3  27684  usgr2wspthons3  27737  clwwlkccatlem  27761  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  erclwwlktr  27794  clwwlkinwwlk  27812  clwwlkf  27820  clwwlkf1  27822  wwlksext2clwwlk  27830  clwwlknscsh  27835  umgr2cwwk2dif  27837  erclwwlkntr  27844  clwwlknonex2  27882  uhgr3cyclex  27955  upgr4cycl4dv4e  27958  eucrctshift  28016  3cyclfrgrrn1  28058  frgrwopreglem2  28086  frgrwopreglem5  28094  frgrwopreglem5ALT  28095  numclwwlk1lem2fo  28131  numclwlk2lem2f  28150  numclwlk2lem2f1o  28152  frgrreg  28167  friendshipgt3  28171  friendship  28172  ipasslem1  28602  shmodsi  29160  elspansn5  29345  h1datomi  29352  nmopsetretALT  29634  pjss2coi  29935  pj3cor1i  29980  mdexchi  30106  atcvat4i  30168  mdsymlem3  30176  mdsymlem4  30177  sumdmdii  30186  cdj3lem2b  30208  elabreximd  30264  iuninc  30306  iundisjf  30333  xrsmulgzz  30660  gsumle  30720  gsumvsca1  30849  gsumvsca2  30850  ofldchr  30882  locfinreflem  31099  xrge0iifiso  31173  lmxrge0  31190  esumfzf  31323  sigaclfu2  31375  signstfvneq0  31837  satfrel  32609  satfrnmapom  32612  fmlafvel  32627  fmlasuc  32628  bccolsum  32966  faclimlem1  32970  dftrpred3g  33067  nosupbnd1  33209  nosupbnd2  33211  segletr  33570  segleantisym  33571  outsideoftr  33585  exp5d  33645  elicc3  33660  finxpreclem2  34665  wl-sbcom2d  34791  poimirlem26  34912  mblfinlem3  34925  itg2addnc  34940  indexa  35002  ax12indalem  36075  ax12inda2ALT  36076  cvrat4  36573  elpaddn0  36930  paddasslem5  36954  paddasslem14  36963  eldioph2  39352  pell1234qrdich  39451  gneispb  40474  rexlimd3  41406  rexabslelem  41685  climsuselem1  41881  stoweidlem19  42298  stoweidlem20  42299  stoweidlem34  42313  wallispilem3  42346  sge0iunmpt  42694  meaiuninc3v  42760  smflimmpt  43078  or2expropbilem1  43261  2reu8i  43306  2elfz2melfz  43512  subsubelfzo0  43520  iccpartigtl  43577  iccpartgt  43581  icceuelpartlem  43589  fargshiftf1  43595  ich2exprop  43627  ichreuopeq  43629  lighneallem3  43766  gbowgt5  43921  bgoldbtbndlem3  43966  bgoldbtbndlem4  43967  bgoldbtbnd  43968  tgblthelfgott  43974  isomuspgrlem2b  43988  upgrwlkupwlk  44009  2zrngagrp  44208  rhmsubcrngclem2  44293  nzerooringczr  44337  lmodvsmdi  44424  ply1mulgsumlem1  44434  elfzolborelfzop1  44568  nnolog2flm1  44644  nn0sumshdiglemA  44673  eenglngeehlnmlem2  44719