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  3186  mob2  3703  reuind  3741  reupick3  4310  elpwunsn  4665  disjiun  5112  sotr2  5600  wefrc  5653  relop  5835  predpoirr  6327  predfrirr  6328  fnun  6657  mpteqb  7010  tpres  7198  fconst5  7203  funfvima  7227  riotaeqimp  7393  dfwe2  7773  limuni3  7852  tfisi  7859  trom  7875  funcnvuni  7933  resf1ext2b  7936  f1oweALT  7976  frxp  8130  poxp  8132  poxp2  8147  poxp3  8154  wfr3g  8326  wfrlem12OLD  8339  onfununi  8360  tz7.48lem  8460  oecl  8554  oaordex  8575  oaass  8578  omwordri  8589  odi  8596  omass  8597  omeu  8602  oen0  8603  oewordi  8608  oewordri  8609  nnarcl  8633  nnmass  8641  brinxper  8753  findcard2  9183  rex2dom  9259  dif1ennnALT  9288  unblem1  9305  unblem2  9306  domunfican  9338  marypha1lem  9450  supiso  9493  inf3lem3  9649  epfrs  9750  frr3g  9775  karden  9914  infxpenlem  10032  iunfictbso  10133  dfac5  10148  dfac2b  10150  kmlem1  10170  kmlem9  10178  infpssrlem3  10324  fin23lem25  10343  fin23lem30  10361  domtriomlem  10461  axdc3lem4  10472  axcclem  10476  zorn2lem7  10521  konigthlem  10587  wunr1om  10738  tskr1om  10786  gruen  10831  grur1a  10838  indpi  10926  genpnmax  11026  prlem934  11052  ltaddpr  11053  ltexprlem7  11061  ltaprlem  11063  axrrecex  11182  axpre-sup  11188  lelttr  11330  dedekind  11403  addlid  11423  nn0lt2  12661  fzind  12696  fnn0ind  12697  btwnz  12701  uzwo  12932  lbzbi  12957  rpnnen1lem5  13002  ledivge1le  13085  xrlelttr  13177  qbtwnre  13220  xrsupsslem  13328  xrinfmsslem  13329  supxrun  13337  elfz1b  13615  elfz0ubfz0  13654  elfzo0z  13723  fzofzim  13731  elfznelfzo  13793  fleqceilz  13876  fsequb  13998  leexp2r  14197  bernneq  14252  fi1uzind  14530  brfi1indALT  14533  swrdnd0  14680  swrdswrdlem  14727  swrdswrd  14728  wrd2ind  14746  swrdccatin1  14748  swrdccatin2  14752  pfxccatin12lem3  14755  repswswrd  14807  cshweqrep  14844  swrd2lsw  14976  2swrd2eqwrdeq  14977  wrdl3s3  14986  s3iunsndisj  14992  cau3lem  15378  climuni  15573  mulcn2  15617  dvdsabseq  16337  divalglem8  16424  ndvdssub  16433  rplpwr  16582  algcvgblem  16601  lcmf  16657  lcmftp  16660  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  lcmfdvdsb  16667  lcmfun  16669  euclemma  16737  prmlem1a  17131  setsstruct2  17198  iscatd  17690  initoeu1  18029  initoeu2  18034  termoeu1  18036  plelttr  18359  insubm  18801  grpinveu  18962  cyccom  19191  symgfixelsi  19421  efgred  19734  telgsumfzs  19975  srgmulgass  20182  srgbinom  20196  lspdisjb  21092  mplcoe5lem  22002  cply1mul  22239  coe1fzgsumd  22247  gsummoncoe1  22251  evl1gsumd  22300  cpmatacl  22659  cpmatmcllem  22661  basis2  22894  0ntr  23014  uncmp  23346  1stcrest  23396  txcls  23547  txcnp  23563  tx1stc  23593  fgss2  23817  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  metcnp3  24484  tngngp3  24600  reconn  24773  iscau4  25236  ellimc3  25837  ulmbdd  26364  ulmcn  26365  sinq12ge0  26474  gausslemma2dlem3  27336  2sq2  27401  2sqreultlem  27415  2sqreunnltlem  27418  ssltleft  27839  ssltright  27840  noseqind  28243  expsgt0  28379  ax5seglem5  28917  ax5seg  28922  uhgrnbgr0nb  29338  cplgrop  29421  wlkl1loop  29623  uspgr2wlkeq  29631  upgrwlkdvdelem  29723  uhgrwkspthlem2  29741  pthdlem2lem  29754  uspgrn2crct  29795  wlkiswwlks2lem3  29858  wlkiswwlks2  29862  wlkiswwlksupgr2  29864  wlklnwwlkln2lem  29869  wwlksnext  29880  wwlksnextfun  29885  rusgrnumwwlk  29962  clwlkclwwlklem2a4  29983  clwlkclwwlklem3  29987  erclwwlksym  30007  erclwwlknsym  30056  eleclclwwlkn  30062  clwwlknonwwlknonb  30092  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  conngrv2edg  30181  eupth2lem3lem6  30219  frgrncvvdeqlem8  30292  frgrwopreglem4a  30296  frgrreggt1  30379  frgrreg  30380  grpoinveu  30505  ococss  31279  shmodsi  31375  h1datomi  31567  hoaddsub  31802  adjmul  32078  chjatom  32343  atomli  32368  atcvat4i  32383  mdsymlem3  32391  mdsymlem5  32393  mdsymlem6  32394  sumdmdlem  32404  cdj3lem2a  32422  cdj3lem3a  32425  bnj1204  35048  umgr2cycllem  35167  umgr2cycl  35168  cvmsdisj  35297  satfv0fun  35398  satffunlem  35428  satffunlem1lem2  35430  satffunlem2lem2  35433  fundmpss  35789  dfon2lem6  35811  dfon2lem8  35813  ifscgr  36067  lineext  36099  fscgr  36103  idinside  36107  btwnconn1lem11  36120  btwnconn1lem12  36121  btwnconn3  36126  brsegle  36131  seglecgr12  36134  hilbert1.2  36178  exp5d  36325  exp5k  36327  nn0prpwlem  36345  bj-restb  37117  exrecfnlem  37402  poimirlem26  37675  poimirlem29  37678  poimirlem32  37681  areacirc  37742  heibor1lem  37838  pridl  38066  pridlc  38100  dmnnzd  38104  disjlem17  38822  membpartlem19  38834  prtlem11  38889  prtlem17  38899  ax12indn  38966  atcvrj0  39452  cvrat4  39467  athgt  39480  lplnexllnN  39588  2llnjN  39591  lvolnle3at  39606  lncmp  39807  paddclN  39866  pexmidlem4N  39997  cdleme17d3  40520  cdleme50trn2  40575  cdlemf2  40586  cdlemf  40587  cdlemj3  40847  cdlemk26b-3  40929  dihord5b  41283  isnacs3  42708  jm2.26  43001  ordnexbtwnsuc  43266  omabs2  43331  naddgeoa  43393  sbiota1  44433  exbir  44479  tratrb  44536  onfrALT  44549  in2an  44608  pwtrrVD  44824  suctrALT2VD  44835  suctrALT2  44836  tratrbVD  44860  trintALTVD  44879  trintALT  44880  or2expropbi  47043  fcoresf1  47078  2reu8i  47122  2reuimp  47124  zm1nn  47311  2ffzoeq  47336  iccpartiltu  47416  iccpartigtl  47417  iccpartgt  47421  iccpartnel  47432  sbcpr  47515  fmtnofac2lem  47562  fmtnofac2  47563  lighneallem2  47600  odd2prm2  47712  stgoldbwt  47770  sbgoldbst  47772  sbgoldbaltlem1  47773  mogoldbb  47779  uhgrimisgrgric  47924  clnbgrgrim  47927  grimedg  47928  gpgedgvtx1  48046  lidldomn1  48186  ply1mulgsumlem1  48342  lincsumcl  48387  ellcoellss  48391  islinindfis  48405  lindslinindsimp1  48413  lindslinindsimp2lem5  48418  lindsrng01  48424  elfzolborelfzop1  48475  rrx2linest  48702  aacllem  49645