Theorem expd 415

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 414	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  expcomd  416  exp32  420  exp4b  430  exp4c  432  exp4d  433  exp42  435  exp44  437  exp5c  444  exp5j  445  exp5l  446  pm3.3  448  expdimp  452  impl  455  syland  603  mpan2d  694  a2and  845  3impib  1116  exp5o  1356  ralrimivv  3175  mob2  3671  reuind  3709  reupick3  4281  elpwunsn  4638  disjiun  5083  sotr2  5563  wefrc  5615  relop  5797  predpoirr  6288  predfrirr  6289  fnun  6603  mpteqb  6957  tpres  7144  fconst5  7149  funfvima  7173  riotaeqimp  7338  dfwe2  7716  limuni3  7791  tfisi  7798  trom  7814  funcnvuni  7871  resf1ext2b  7874  f1oweALT  7913  frxp  8065  poxp  8067  poxp2  8082  poxp3  8089  wfr3g  8258  onfununi  8270  tz7.48lem  8369  oecl  8461  oaordex  8482  oaass  8485  omwordri  8496  odi  8503  omass  8504  omeu  8509  oen0  8510  oewordi  8515  oewordri  8516  nnarcl  8540  nnmass  8548  brinxper  8660  findcard2  9084  rex2dom  9147  dif1ennnALT  9171  unblem1  9186  unblem2  9187  domunfican  9216  marypha1lem  9327  supiso  9370  inf3lem3  9530  epfrs  9631  frr3g  9659  karden  9798  infxpenlem  9914  iunfictbso  10015  dfac5  10030  dfac2b  10032  kmlem1  10052  kmlem9  10060  infpssrlem3  10206  fin23lem25  10225  fin23lem30  10243  domtriomlem  10343  axdc3lem4  10354  axcclem  10358  zorn2lem7  10403  konigthlem  10469  wunr1om  10620  tskr1om  10668  gruen  10713  grur1a  10720  indpi  10808  genpnmax  10908  prlem934  10934  ltaddpr  10935  ltexprlem7  10943  ltaprlem  10945  axrrecex  11064  axpre-sup  11070  lelttr  11213  dedekind  11286  addlid  11306  nn0lt2  12546  fzind  12581  fnn0ind  12582  btwnz  12586  uzwo  12819  lbzbi  12844  rpnnen1lem5  12889  ledivge1le  12973  xrlelttr  13065  qbtwnre  13108  xrsupsslem  13216  xrinfmsslem  13217  supxrun  13225  elfz1b  13503  elfz0ubfz0  13542  elfzo0z  13611  fzofzim  13619  elfznelfzo  13683  fleqceilz  13768  fsequb  13892  leexp2r  14091  bernneq  14146  fi1uzind  14424  brfi1indALT  14427  swrdnd0  14575  swrdswrdlem  14621  swrdswrd  14622  wrd2ind  14640  swrdccatin1  14642  swrdccatin2  14646  pfxccatin12lem3  14649  repswswrd  14701  cshweqrep  14738  swrd2lsw  14869  2swrd2eqwrdeq  14870  wrdl3s3  14879  s3iunsndisj  14885  cau3lem  15272  climuni  15469  mulcn2  15513  dvdsabseq  16234  divalglem8  16321  ndvdssub  16330  rplpwr  16479  algcvgblem  16498  lcmf  16554  lcmftp  16557  lcmfunsnlem2lem1  16559  lcmfunsnlem2lem2  16560  lcmfdvdsb  16564  lcmfun  16566  euclemma  16634  prmlem1a  17028  setsstruct2  17095  iscatd  17589  initoeu1  17928  initoeu2  17933  termoeu1  17935  plelttr  18258  insubm  18736  grpinveu  18897  cyccom  19125  symgfixelsi  19357  efgred  19670  telgsumfzs  19911  srgmulgass  20145  srgbinom  20159  lspdisjb  21073  mplcoe5lem  21984  cply1mul  22221  coe1fzgsumd  22229  gsummoncoe1  22233  evl1gsumd  22282  cpmatacl  22641  cpmatmcllem  22643  basis2  22876  0ntr  22996  uncmp  23328  1stcrest  23378  txcls  23529  txcnp  23545  tx1stc  23575  fgss2  23799  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALTlem4  23975  metcnp3  24465  tngngp3  24581  reconn  24754  iscau4  25216  ellimc3  25817  ulmbdd  26344  ulmcn  26345  sinq12ge0  26454  gausslemma2dlem3  27316  2sq2  27381  2sqreultlem  27395  2sqreunnltlem  27398  ssltleft  27825  ssltright  27826  noseqind  28232  expsgt0  28370  ax5seglem5  28922  ax5seg  28927  uhgrnbgr0nb  29343  cplgrop  29426  wlkl1loop  29627  uspgr2wlkeq  29635  upgrwlkdvdelem  29725  uhgrwkspthlem2  29743  pthdlem2lem  29756  uspgrn2crct  29797  wlkiswwlks2lem3  29860  wlkiswwlks2  29864  wlkiswwlksupgr2  29866  wlklnwwlkln2lem  29871  wwlksnext  29882  wwlksnextfun  29887  rusgrnumwwlk  29967  clwlkclwwlklem2a4  29988  clwlkclwwlklem3  29992  erclwwlksym  30012  erclwwlknsym  30061  eleclclwwlkn  30067  clwwlknonwwlknonb  30097  upgr3v3e3cycl  30171  upgr4cycl4dv4e  30176  conngrv2edg  30186  eupth2lem3lem6  30224  frgrncvvdeqlem8  30297  frgrwopreglem4a  30301  frgrreggt1  30384  frgrreg  30385  grpoinveu  30510  ococss  31284  shmodsi  31380  h1datomi  31572  hoaddsub  31807  adjmul  32083  chjatom  32348  atomli  32373  atcvat4i  32388  mdsymlem3  32396  mdsymlem5  32398  mdsymlem6  32399  sumdmdlem  32409  cdj3lem2a  32427  cdj3lem3a  32430  bnj1204  35035  umgr2cycllem  35195  umgr2cycl  35196  cvmsdisj  35325  satfv0fun  35426  satffunlem  35456  satffunlem1lem2  35458  satffunlem2lem2  35461  fundmpss  35822  dfon2lem6  35841  dfon2lem8  35843  ifscgr  36099  lineext  36131  fscgr  36135  idinside  36139  btwnconn1lem11  36152  btwnconn1lem12  36153  btwnconn3  36158  brsegle  36163  seglecgr12  36166  hilbert1.2  36210  exp5d  36357  exp5k  36359  nn0prpwlem  36377  bj-restb  37149  exrecfnlem  37434  poimirlem26  37696  poimirlem29  37699  poimirlem32  37702  areacirc  37763  heibor1lem  37859  pridl  38087  pridlc  38121  dmnnzd  38125  disjlem17  38907  membpartlem19  38919  prtlem11  38975  prtlem17  38985  ax12indn  39052  atcvrj0  39537  cvrat4  39552  athgt  39565  lplnexllnN  39673  2llnjN  39676  lvolnle3at  39691  lncmp  39892  paddclN  39951  pexmidlem4N  40082  cdleme17d3  40605  cdleme50trn2  40660  cdlemf2  40671  cdlemf  40672  cdlemj3  40932  cdlemk26b-3  41014  dihord5b  41368  isnacs3  42817  jm2.26  43109  ordnexbtwnsuc  43374  omabs2  43439  naddgeoa  43501  sbiota1  44541  exbir  44586  tratrb  44643  onfrALT  44656  in2an  44715  pwtrrVD  44931  suctrALT2VD  44942  suctrALT2  44943  tratrbVD  44967  trintALTVD  44986  trintALT  44987  or2expropbi  47148  fcoresf1  47183  2reu8i  47227  2reuimp  47229  zm1nn  47416  2ffzoeq  47441  iccpartiltu  47536  iccpartigtl  47537  iccpartgt  47541  iccpartnel  47552  sbcpr  47635  fmtnofac2lem  47682  fmtnofac2  47683  lighneallem2  47720  odd2prm2  47832  stgoldbwt  47890  sbgoldbst  47892  sbgoldbaltlem1  47893  mogoldbb  47899  uhgrimisgrgric  48045  clnbgrgrim  48048  grimedg  48049  gpgedgvtx1  48176  gpgedg2iv  48181  pgnbgreunbgrlem3  48232  pgnbgreunbgrlem6  48238  pgnbgreunbgr  48239  lidldomn1  48345  ply1mulgsumlem1  48501  lincsumcl  48546  ellcoellss  48550  islinindfis  48564  lindslinindsimp1  48572  lindslinindsimp2lem5  48577  lindsrng01  48583  elfzolborelfzop1  48634  rrx2linest  48857  aacllem  49916