Theorem expd 417

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)

Hypothesis

Ref	Expression
expd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expdcom 416	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  expcomd  418  exp32  422  exp4b  432  exp4c  434  exp4d  435  exp42  437  exp44  439  exp5c  446  exp5j  447  exp5l  448  pm3.3  450  expdimp  454  impl  457  syland  604  mpan2d  693  a2and  844  3impib  1117  exp5o  1356  ralrimivv  3199  mob2  3711  reuind  3749  reupick3  4319  elpwunsn  4687  disjiun  5135  sotr2  5620  wefrc  5670  relop  5849  predpoirr  6332  predfrirr  6333  fnun  6661  mpteqb  7015  tpres  7199  fconst5  7204  funfvima  7229  riotaeqimp  7389  dfwe2  7758  limuni3  7838  tfisi  7845  trom  7861  funcnvuni  7919  f1oweALT  7956  frxp  8109  poxp  8111  poxp2  8126  poxp3  8133  wfr3g  8304  wfrlem12OLD  8317  onfununi  8338  tz7.48lem  8438  oecl  8534  oaordex  8555  oaass  8558  omwordri  8569  odi  8576  omass  8577  omeu  8582  oen0  8583  oewordi  8588  oewordri  8589  nnarcl  8613  nnmass  8621  findcard2  9161  rex2dom  9243  dif1ennnALT  9274  findcard2OLD  9281  unblem1  9292  unblem2  9293  domunfican  9317  marypha1lem  9425  supiso  9467  inf3lem3  9622  epfrs  9723  frr3g  9748  karden  9887  infxpenlem  10005  iunfictbso  10106  dfac5  10120  dfac2b  10122  kmlem1  10142  kmlem9  10150  infpssrlem3  10297  fin23lem25  10316  fin23lem30  10334  domtriomlem  10434  axdc3lem4  10445  axcclem  10449  zorn2lem7  10494  konigthlem  10560  wunr1om  10711  tskr1om  10759  gruen  10804  grur1a  10811  indpi  10899  genpnmax  10999  prlem934  11025  ltaddpr  11026  ltexprlem7  11034  ltaprlem  11036  axrrecex  11155  axpre-sup  11161  lelttr  11301  dedekind  11374  addlid  11394  nn0lt2  12622  fzind  12657  fnn0ind  12658  btwnz  12662  uzwo  12892  lbzbi  12917  rpnnen1lem5  12962  ledivge1le  13042  xrlelttr  13132  qbtwnre  13175  xrsupsslem  13283  xrinfmsslem  13284  supxrun  13292  elfz1b  13567  elfz0ubfz0  13602  elfzo0z  13671  fzofzim  13676  elfznelfzo  13734  fleqceilz  13816  fsequb  13937  leexp2r  14136  bernneq  14189  fi1uzind  14455  brfi1indALT  14458  swrdnd0  14604  swrdswrdlem  14651  swrdswrd  14652  wrd2ind  14670  swrdccatin1  14672  swrdccatin2  14676  pfxccatin12lem3  14679  repswswrd  14731  cshweqrep  14768  swrd2lsw  14900  2swrd2eqwrdeq  14901  wrdl3s3  14910  s3iunsndisj  14912  cau3lem  15298  climuni  15493  mulcn2  15537  dvdsabseq  16253  divalglem8  16340  ndvdssub  16349  rplpwr  16496  algcvgblem  16511  lcmf  16567  lcmftp  16570  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  lcmfdvdsb  16577  lcmfun  16579  euclemma  16647  prmlem1a  17037  setsstruct2  17104  iscatd  17614  initoeu1  17958  initoeu2  17963  termoeu1  17965  plelttr  18294  insubm  18696  grpinveu  18856  cyccom  19075  symgfixelsi  19298  efgred  19611  telgsumfzs  19852  srgmulgass  20034  srgbinom  20048  lspdisjb  20732  mplcoe5lem  21586  cply1mul  21810  coe1fzgsumd  21818  gsummoncoe1  21820  evl1gsumd  21868  cpmatacl  22210  cpmatmcllem  22212  basis2  22446  0ntr  22567  uncmp  22899  1stcrest  22949  txcls  23100  txcnp  23116  tx1stc  23146  fgss2  23370  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  metcnp3  24041  tngngp3  24165  reconn  24336  iscau4  24788  ellimc3  25388  ulmbdd  25902  ulmcn  25903  sinq12ge0  26010  gausslemma2dlem3  26861  2sq2  26926  2sqreultlem  26940  2sqreunnltlem  26943  ssltleft  27355  ssltright  27356  ax5seglem5  28181  ax5seg  28186  uhgrnbgr0nb  28601  cplgrop  28684  wlkl1loop  28885  uspgr2wlkeq  28893  upgrwlkdvdelem  28983  uhgrwkspthlem2  29001  pthdlem2lem  29014  uspgrn2crct  29052  wlkiswwlks2lem3  29115  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wlklnwwlkln2lem  29126  wwlksnext  29137  wwlksnextfun  29142  rusgrnumwwlk  29219  clwlkclwwlklem2a4  29240  clwlkclwwlklem3  29244  erclwwlksym  29264  erclwwlknsym  29313  eleclclwwlkn  29319  clwwlknonwwlknonb  29349  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  conngrv2edg  29438  eupth2lem3lem6  29476  frgrncvvdeqlem8  29549  frgrwopreglem4a  29553  frgrreggt1  29636  frgrreg  29637  grpoinveu  29760  ococss  30534  shmodsi  30630  h1datomi  30822  hoaddsub  31057  adjmul  31333  chjatom  31598  atomli  31623  atcvat4i  31638  mdsymlem3  31646  mdsymlem5  31648  mdsymlem6  31649  sumdmdlem  31659  cdj3lem2a  31677  cdj3lem3a  31680  bnj1204  34012  umgr2cycllem  34120  umgr2cycl  34121  cvmsdisj  34250  satfv0fun  34351  satffunlem  34381  satffunlem1lem2  34383  satffunlem2lem2  34386  fundmpss  34727  dfon2lem6  34749  dfon2lem8  34751  ifscgr  35005  lineext  35037  fscgr  35041  idinside  35045  btwnconn1lem11  35058  btwnconn1lem12  35059  btwnconn3  35064  brsegle  35069  seglecgr12  35072  hilbert1.2  35116  exp5d  35176  exp5k  35178  nn0prpwlem  35196  bj-restb  35964  exrecfnlem  36249  poimirlem26  36503  poimirlem29  36506  poimirlem32  36509  areacirc  36570  heibor1lem  36666  pridl  36894  pridlc  36928  dmnnzd  36932  disjlem17  37658  membpartlem19  37670  prtlem11  37725  prtlem17  37735  ax12indn  37802  atcvrj0  38288  cvrat4  38303  athgt  38316  lplnexllnN  38424  2llnjN  38427  lvolnle3at  38442  lncmp  38643  paddclN  38702  pexmidlem4N  38833  cdleme17d3  39356  cdleme50trn2  39411  cdlemf2  39422  cdlemf  39423  cdlemj3  39683  cdlemk26b-3  39765  dihord5b  40119  isnacs3  41434  jm2.26  41727  ordnexbtwnsuc  42003  omabs2  42068  naddgeoa  42131  sbiota1  43179  exbir  43225  tratrb  43283  onfrALT  43296  in2an  43355  pwtrrVD  43572  suctrALT2VD  43583  suctrALT2  43584  tratrbVD  43608  trintALTVD  43627  trintALT  43628  or2expropbi  45731  fcoresf1  45766  2reu8i  45808  2reuimp  45810  zm1nn  45997  2ffzoeq  46023  iccpartiltu  46077  iccpartigtl  46078  iccpartgt  46082  iccpartnel  46093  sbcpr  46176  fmtnofac2lem  46223  fmtnofac2  46224  lighneallem2  46261  odd2prm2  46373  stgoldbwt  46431  sbgoldbst  46433  sbgoldbaltlem1  46434  mogoldbb  46440  isomuspgrlem1  46482  isomuspgrlem2d  46486  lidldomn1  46777  ply1mulgsumlem1  47021  lincsumcl  47066  ellcoellss  47070  islinindfis  47084  lindslinindsimp1  47092  lindslinindsimp2lem5  47097  lindsrng01  47103  elfzolborelfzop1  47154  rrx2linest  47382  aacllem  47802