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  3712  reuind  3750  reupick3  4320  elpwunsn  4688  disjiun  5136  sotr2  5621  wefrc  5671  relop  5851  predpoirr  6335  predfrirr  6336  fnun  6664  mpteqb  7018  tpres  7202  fconst5  7207  funfvima  7232  riotaeqimp  7392  dfwe2  7761  limuni3  7841  tfisi  7848  trom  7864  funcnvuni  7922  f1oweALT  7959  frxp  8112  poxp  8114  poxp2  8129  poxp3  8136  wfr3g  8307  wfrlem12OLD  8320  onfununi  8341  tz7.48lem  8441  oecl  8537  oaordex  8558  oaass  8561  omwordri  8572  odi  8579  omass  8580  omeu  8585  oen0  8586  oewordi  8591  oewordri  8592  nnarcl  8616  nnmass  8624  findcard2  9164  rex2dom  9246  dif1ennnALT  9277  findcard2OLD  9284  unblem1  9295  unblem2  9296  domunfican  9320  marypha1lem  9428  supiso  9470  inf3lem3  9625  epfrs  9726  frr3g  9751  karden  9890  infxpenlem  10008  iunfictbso  10109  dfac5  10123  dfac2b  10125  kmlem1  10145  kmlem9  10153  infpssrlem3  10300  fin23lem25  10319  fin23lem30  10337  domtriomlem  10437  axdc3lem4  10448  axcclem  10452  zorn2lem7  10497  konigthlem  10563  wunr1om  10714  tskr1om  10762  gruen  10807  grur1a  10814  indpi  10902  genpnmax  11002  prlem934  11028  ltaddpr  11029  ltexprlem7  11037  ltaprlem  11039  axrrecex  11158  axpre-sup  11164  lelttr  11304  dedekind  11377  addlid  11397  nn0lt2  12625  fzind  12660  fnn0ind  12661  btwnz  12665  uzwo  12895  lbzbi  12920  rpnnen1lem5  12965  ledivge1le  13045  xrlelttr  13135  qbtwnre  13178  xrsupsslem  13286  xrinfmsslem  13287  supxrun  13295  elfz1b  13570  elfz0ubfz0  13605  elfzo0z  13674  fzofzim  13679  elfznelfzo  13737  fleqceilz  13819  fsequb  13940  leexp2r  14139  bernneq  14192  fi1uzind  14458  brfi1indALT  14461  swrdnd0  14607  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  swrdccatin2  14679  pfxccatin12lem3  14682  repswswrd  14734  cshweqrep  14771  swrd2lsw  14903  2swrd2eqwrdeq  14904  wrdl3s3  14913  s3iunsndisj  14915  cau3lem  15301  climuni  15496  mulcn2  15540  dvdsabseq  16256  divalglem8  16343  ndvdssub  16352  rplpwr  16499  algcvgblem  16514  lcmf  16570  lcmftp  16573  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfdvdsb  16580  lcmfun  16582  euclemma  16650  prmlem1a  17040  setsstruct2  17107  iscatd  17617  initoeu1  17961  initoeu2  17966  termoeu1  17968  plelttr  18297  insubm  18699  grpinveu  18859  cyccom  19080  symgfixelsi  19303  efgred  19616  telgsumfzs  19857  srgmulgass  20040  srgbinom  20054  lspdisjb  20739  mplcoe5lem  21594  cply1mul  21818  coe1fzgsumd  21826  gsummoncoe1  21828  evl1gsumd  21876  cpmatacl  22218  cpmatmcllem  22220  basis2  22454  0ntr  22575  uncmp  22907  1stcrest  22957  txcls  23108  txcnp  23124  tx1stc  23154  fgss2  23378  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  metcnp3  24049  tngngp3  24173  reconn  24344  iscau4  24796  ellimc3  25396  ulmbdd  25910  ulmcn  25911  sinq12ge0  26018  gausslemma2dlem3  26871  2sq2  26936  2sqreultlem  26950  2sqreunnltlem  26953  ssltleft  27365  ssltright  27366  ax5seglem5  28191  ax5seg  28196  uhgrnbgr0nb  28611  cplgrop  28694  wlkl1loop  28895  uspgr2wlkeq  28903  upgrwlkdvdelem  28993  uhgrwkspthlem2  29011  pthdlem2lem  29024  uspgrn2crct  29062  wlkiswwlks2lem3  29125  wlkiswwlks2  29129  wlkiswwlksupgr2  29131  wlklnwwlkln2lem  29136  wwlksnext  29147  wwlksnextfun  29152  rusgrnumwwlk  29229  clwlkclwwlklem2a4  29250  clwlkclwwlklem3  29254  erclwwlksym  29274  erclwwlknsym  29323  eleclclwwlkn  29329  clwwlknonwwlknonb  29359  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  conngrv2edg  29448  eupth2lem3lem6  29486  frgrncvvdeqlem8  29559  frgrwopreglem4a  29563  frgrreggt1  29646  frgrreg  29647  grpoinveu  29772  ococss  30546  shmodsi  30642  h1datomi  30834  hoaddsub  31069  adjmul  31345  chjatom  31610  atomli  31635  atcvat4i  31650  mdsymlem3  31658  mdsymlem5  31660  mdsymlem6  31661  sumdmdlem  31671  cdj3lem2a  31689  cdj3lem3a  31692  bnj1204  34023  umgr2cycllem  34131  umgr2cycl  34132  cvmsdisj  34261  satfv0fun  34362  satffunlem  34392  satffunlem1lem2  34394  satffunlem2lem2  34397  fundmpss  34738  dfon2lem6  34760  dfon2lem8  34762  ifscgr  35016  lineext  35048  fscgr  35052  idinside  35056  btwnconn1lem11  35069  btwnconn1lem12  35070  btwnconn3  35075  brsegle  35080  seglecgr12  35083  hilbert1.2  35127  exp5d  35187  exp5k  35189  nn0prpwlem  35207  bj-restb  35975  exrecfnlem  36260  poimirlem26  36514  poimirlem29  36517  poimirlem32  36520  areacirc  36581  heibor1lem  36677  pridl  36905  pridlc  36939  dmnnzd  36943  disjlem17  37669  membpartlem19  37681  prtlem11  37736  prtlem17  37746  ax12indn  37813  atcvrj0  38299  cvrat4  38314  athgt  38327  lplnexllnN  38435  2llnjN  38438  lvolnle3at  38453  lncmp  38654  paddclN  38713  pexmidlem4N  38844  cdleme17d3  39367  cdleme50trn2  39422  cdlemf2  39433  cdlemf  39434  cdlemj3  39694  cdlemk26b-3  39776  dihord5b  40130  isnacs3  41448  jm2.26  41741  ordnexbtwnsuc  42017  omabs2  42082  naddgeoa  42145  sbiota1  43193  exbir  43239  tratrb  43297  onfrALT  43310  in2an  43369  pwtrrVD  43586  suctrALT2VD  43597  suctrALT2  43598  tratrbVD  43622  trintALTVD  43641  trintALT  43642  or2expropbi  45744  fcoresf1  45779  2reu8i  45821  2reuimp  45823  zm1nn  46010  2ffzoeq  46036  iccpartiltu  46090  iccpartigtl  46091  iccpartgt  46095  iccpartnel  46106  sbcpr  46189  fmtnofac2lem  46236  fmtnofac2  46237  lighneallem2  46274  odd2prm2  46386  stgoldbwt  46444  sbgoldbst  46446  sbgoldbaltlem1  46447  mogoldbb  46453  isomuspgrlem1  46495  isomuspgrlem2d  46499  lidldomn1  46823  ply1mulgsumlem1  47067  lincsumcl  47112  ellcoellss  47116  islinindfis  47130  lindslinindsimp1  47138  lindslinindsimp2lem5  47143  lindsrng01  47149  elfzolborelfzop1  47200  rrx2linest  47428  aacllem  47848