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  653  exbiri  810  3exp  1116  exp516  1353  rexlimdva2  3246  r19.29af2  3288  reusv2lem2  5265  pwssun  5421  onmindif  6248  mpteqb  6764  fliftfun  7044  elovmpt3rab1  7385  ordsucss  7513  tfindsg  7555  imacosuppOLD  7858  tfrlem1  7995  tfrlem9  8004  oaordi  8155  oaordex  8167  oaass  8170  oarec  8171  omass  8189  oen0  8195  oeordsuc  8203  nnaordi  8227  omsmolem  8263  infensuc  8679  php3  8687  suppeqfsuppbi  8831  marypha1lem  8881  hartogs  8992  card2on  9002  tz9.12lem3  9202  infxpenlem  9424  cfcoflem  9683  isf32lem12  9775  zorn2lem6  9912  ondomon  9974  axrepnd  10005  fpwwe2lem12  10052  genpcd  10417  ltexprlem6  10452  axpre-sup  10580  negf1o  11059  recex  11261  uzaddcl  12292  nn01to3  12329  rpnnen1lem5  12368  xrsupsslem  12688  xrinfmsslem  12689  supxrunb1  12700  supxrunb2  12701  fz0fzelfz0  13008  fz0fzdiffz0  13011  elfzmlbp  13013  difelfzle  13015  fzo1fzo0n0  13083  elincfzoext  13090  ssfzo12bi  13127  elfznelfzo  13137  modaddmodup  13297  modfzo0difsn  13306  fsuppmapnn0fiubex  13355  seqf1o  13407  expcllem  13436  expeq0  13455  mulexp  13464  hashgt12el2  13780  hashimarni  13798  hash2prd  13829  fi1uzind  13851  swrdnd  14007  swrdswrdlem  14057  swrdswrd  14058  pfxccat3  14087  reuccatpfxs1  14100  repswswrd  14137  repswccat  14139  cshwidxmod  14156  2cshwcshw  14178  s4f1o  14271  wwlktovfo  14313  relexpindlem  14414  resqrex  14602  summo  15066  fsum2d  15118  modfsummods  15140  binom  15177  clim2prod  15236  fprod2d  15327  binomfallfac  15387  efexp  15446  demoivreALT  15546  divconjdvds  15657  addmodlteqALT  15667  dfgcd2  15884  lcmfunsnlem2lem1  15972  lcmfdvdsb  15977  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  oddprmdvds  16229  ramcl  16355  prmgaplem6  16382  cshwsidrepswmod0  16420  cshwshashlem1  16421  cshwshashlem2  16422  ressress  16554  initoeu2lem1  17266  symggen  18590  pmtr3ncom  18595  srgmulgass  19274  srgbinom  19288  ringinvnzdiv  19339  lmodvsmmulgdi  19662  psgndiflemB  20289  assamulgscmlem2  20586  mptcoe1fsupp  20844  coe1fzgsumdlem  20930  evl1gsumdlem  20980  scmatmulcl  21123  mdetdiagid  21205  pm2mpf1  21404  mptcoe1matfsupp  21407  mp2pm2mplem4  21414  chpdmat  21446  chfacfisf  21459  chfacfisfcpmat  21460  chcoeffeq  21491  topbas  21577  elcls  21678  elcls3  21688  2ndcdisj  22061  filufint  22525  ovoliunlem3  24108  dvge0  24609  ulmcn  24994  gausslemma2dlem3  25952  sizusglecusg  27253  upgriswlk  27430  2pthnloop  27520  crctcshwlkn0  27607  wlknwwlksnbij  27674  wwlksnred  27678  wwlksnext  27679  wwlksnextinj  27685  wwlksnextproplem2  27696  wwlksnextproplem3  27697  usgr2wspthons3  27750  clwwlkccatlem  27774  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  erclwwlktr  27807  clwwlkinwwlk  27825  clwwlkf  27832  clwwlkf1  27834  wwlksext2clwwlk  27842  clwwlknscsh  27847  umgr2cwwk2dif  27849  erclwwlkntr  27856  clwwlknonex2  27894  uhgr3cyclex  27967  upgr4cycl4dv4e  27970  eucrctshift  28028  3cyclfrgrrn1  28070  frgrwopreglem2  28098  frgrwopreglem5  28106  frgrwopreglem5ALT  28107  numclwwlk1lem2fo  28143  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  frgrreg  28179  friendshipgt3  28183  friendship  28184  ipasslem1  28614  shmodsi  29172  elspansn5  29357  h1datomi  29364  nmopsetretALT  29646  pjss2coi  29947  pj3cor1i  29992  mdexchi  30118  atcvat4i  30180  mdsymlem3  30188  mdsymlem4  30189  sumdmdii  30198  cdj3lem2b  30220  elabreximd  30278  iuninc  30324  iundisjf  30352  xrsmulgzz  30712  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  ofldchr  30938  locfinreflem  31193  xrge0iifiso  31288  lmxrge0  31305  esumfzf  31438  sigaclfu2  31490  signstfvneq0  31952  satfrel  32727  satfrnmapom  32730  fmlafvel  32745  fmlasuc  32746  bccolsum  33084  faclimlem1  33088  dftrpred3g  33185  nosupbnd1  33327  nosupbnd2  33329  segletr  33688  segleantisym  33689  outsideoftr  33703  exp5d  33763  elicc3  33778  finxpreclem2  34807  wl-sbcom2d  34962  poimirlem26  35083  mblfinlem3  35096  itg2addnc  35111  indexa  35171  ax12indalem  36241  ax12inda2ALT  36242  cvrat4  36739  elpaddn0  37096  paddasslem5  37120  paddasslem14  37129  eldioph2  39703  pell1234qrdich  39802  gneispb  40834  rexlimd3  41781  rexabslelem  42055  climsuselem1  42249  stoweidlem19  42661  stoweidlem20  42662  stoweidlem34  42676  wallispilem3  42709  sge0iunmpt  43057  meaiuninc3v  43123  smflimmpt  43441  or2expropbilem1  43624  2reu8i  43669  2elfz2melfz  43875  subsubelfzo0  43883  iccpartigtl  43940  iccpartgt  43944  icceuelpartlem  43952  fargshiftf1  43958  ich2exprop  43988  ichreuopeq  43990  lighneallem3  44125  gbowgt5  44280  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgblthelfgott  44333  isomuspgrlem2b  44347  upgrwlkupwlk  44368  2zrngagrp  44567  rhmsubcrngclem2  44652  nzerooringczr  44696  lmodvsmdi  44784  ply1mulgsumlem1  44794  elfzolborelfzop1  44928  nnolog2flm1  45004  nn0sumshdiglemA  45033  eenglngeehlnmlem2  45152