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 206  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  602  mpan2d  690  a2and  841  3impib  1114  exp5o  1353  ralrimivv  3113  mob2  3645  reuind  3683  reupick3  4250  elpwunsn  4616  disjiun  5057  sotr2  5526  wefrc  5574  relop  5748  predpoirr  6225  predfrirr  6226  fnun  6529  mpteqb  6876  tpres  7058  fconst5  7063  funfvima  7088  riotaeqimp  7239  dfwe2  7602  limuni3  7674  tfisi  7680  trom  7696  funcnvuni  7752  f1oweALT  7788  frxp  7938  poxp  7940  wfr3g  8109  wfrlem12OLD  8122  onfununi  8143  tz7.48lem  8242  oecl  8329  oaordex  8351  oaass  8354  omwordri  8365  odi  8372  omass  8373  omeu  8378  oen0  8379  oewordi  8384  oewordri  8385  nnarcl  8409  nnmass  8417  findcard2  8909  dif1enALT  8980  findcard2OLD  8986  unblem1  8996  unblem2  8997  domunfican  9017  marypha1lem  9122  supiso  9164  inf3lem3  9318  epfrs  9420  frr3g  9445  karden  9584  infxpenlem  9700  iunfictbso  9801  dfac5  9815  dfac2b  9817  kmlem1  9837  kmlem9  9845  infpssrlem3  9992  fin23lem25  10011  fin23lem30  10029  domtriomlem  10129  axdc3lem4  10140  axcclem  10144  zorn2lem7  10189  konigthlem  10255  wunr1om  10406  tskr1om  10454  gruen  10499  grur1a  10506  indpi  10594  genpnmax  10694  prlem934  10720  ltaddpr  10721  ltexprlem7  10729  ltaprlem  10731  axrrecex  10850  axpre-sup  10856  lelttr  10996  dedekind  11068  addid2  11088  nn0lt2  12313  fzind  12348  fnn0ind  12349  btwnz  12352  uzwo  12580  lbzbi  12605  rpnnen1lem5  12650  ledivge1le  12730  xrlelttr  12819  qbtwnre  12862  xrsupsslem  12970  xrinfmsslem  12971  supxrun  12979  elfz1b  13254  elfz0ubfz0  13289  elfzo0z  13357  fzofzim  13362  elfznelfzo  13420  fleqceilz  13502  fsequb  13623  leexp2r  13820  bernneq  13872  fi1uzind  14139  brfi1indALT  14142  swrdnd0  14298  swrdswrdlem  14345  swrdswrd  14346  wrd2ind  14364  swrdccatin1  14366  swrdccatin2  14370  pfxccatin12lem3  14373  repswswrd  14425  cshweqrep  14462  swrd2lsw  14593  2swrd2eqwrdeq  14594  wrdl3s3  14605  s3iunsndisj  14607  cau3lem  14994  climuni  15189  mulcn2  15233  dvdsabseq  15950  divalglem8  16037  ndvdssub  16046  rplpwr  16195  algcvgblem  16210  lcmf  16266  lcmftp  16269  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfdvdsb  16276  lcmfun  16278  euclemma  16346  prmlem1a  16736  setsstruct2  16803  iscatd  17299  initoeu1  17642  initoeu2  17647  termoeu1  17649  plelttr  17977  insubm  18372  grpinveu  18529  cyccom  18737  symgfixelsi  18958  efgred  19269  telgsumfzs  19505  srgmulgass  19682  srgbinom  19696  lspdisjb  20303  mplcoe5lem  21150  cply1mul  21375  coe1fzgsumd  21383  gsummoncoe1  21385  evl1gsumd  21433  cpmatacl  21773  cpmatmcllem  21775  basis2  22009  0ntr  22130  uncmp  22462  1stcrest  22512  txcls  22663  txcnp  22679  tx1stc  22709  fgss2  22933  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  metcnp3  23602  tngngp3  23726  reconn  23897  iscau4  24348  ellimc3  24948  ulmbdd  25462  ulmcn  25463  sinq12ge0  25570  gausslemma2dlem3  26421  2sq2  26486  2sqreultlem  26500  2sqreunnltlem  26503  ax5seglem5  27204  ax5seg  27209  uhgrnbgr0nb  27624  cplgrop  27707  wlkl1loop  27907  uspgr2wlkeq  27915  upgrwlkdvdelem  28005  uhgrwkspthlem2  28023  pthdlem2lem  28036  uspgrn2crct  28074  wlkiswwlks2lem3  28137  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wwlksnext  28159  wwlksnextfun  28164  rusgrnumwwlk  28241  clwlkclwwlklem2a4  28262  clwlkclwwlklem3  28266  erclwwlksym  28286  erclwwlknsym  28335  eleclclwwlkn  28341  clwwlknonwwlknonb  28371  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  conngrv2edg  28460  eupth2lem3lem6  28498  frgrncvvdeqlem8  28571  frgrwopreglem4a  28575  frgrreggt1  28658  frgrreg  28659  grpoinveu  28782  ococss  29556  shmodsi  29652  h1datomi  29844  hoaddsub  30079  adjmul  30355  chjatom  30620  atomli  30645  atcvat4i  30660  mdsymlem3  30668  mdsymlem5  30670  mdsymlem6  30671  sumdmdlem  30681  cdj3lem2a  30699  cdj3lem3a  30702  bnj1204  32892  umgr2cycllem  33002  umgr2cycl  33003  cvmsdisj  33132  satfv0fun  33233  satffunlem  33263  satffunlem1lem2  33265  satffunlem2lem2  33268  fundmpss  33646  dfon2lem6  33670  dfon2lem8  33672  poxp2  33717  poxp3  33723  ssltleft  33981  ssltright  33982  ifscgr  34273  lineext  34305  fscgr  34309  idinside  34313  btwnconn1lem11  34326  btwnconn1lem12  34327  btwnconn3  34332  brsegle  34337  seglecgr12  34340  hilbert1.2  34384  exp5d  34418  exp5k  34420  nn0prpwlem  34438  bj-restb  35192  exrecfnlem  35477  poimirlem26  35730  poimirlem29  35733  poimirlem32  35736  areacirc  35797  heibor1lem  35894  pridl  36122  pridlc  36156  dmnnzd  36160  prtlem11  36807  prtlem17  36817  ax12indn  36884  atcvrj0  37369  cvrat4  37384  athgt  37397  lplnexllnN  37505  2llnjN  37508  lvolnle3at  37523  lncmp  37724  paddclN  37783  pexmidlem4N  37914  cdleme17d3  38437  cdleme50trn2  38492  cdlemf2  38503  cdlemf  38504  cdlemj3  38764  cdlemk26b-3  38846  dihord5b  39200  isnacs3  40448  jm2.26  40740  sbiota1  41941  exbir  41987  tratrb  42045  onfrALT  42058  in2an  42117  pwtrrVD  42334  suctrALT2VD  42345  suctrALT2  42346  tratrbVD  42370  trintALTVD  42389  trintALT  42390  or2expropbi  44415  fcoresf1  44450  2reu8i  44492  2reuimp  44494  zm1nn  44682  2ffzoeq  44708  iccpartiltu  44762  iccpartigtl  44763  iccpartgt  44767  iccpartnel  44778  sbcpr  44861  fmtnofac2lem  44908  fmtnofac2  44909  lighneallem2  44946  odd2prm2  45058  stgoldbwt  45116  sbgoldbst  45118  sbgoldbaltlem1  45119  mogoldbb  45125  isomuspgrlem1  45167  isomuspgrlem2d  45171  lidldomn1  45367  ply1mulgsumlem1  45615  lincsumcl  45660  ellcoellss  45664  islinindfis  45678  lindslinindsimp1  45686  lindslinindsimp2lem5  45691  lindsrng01  45697  elfzolborelfzop1  45748  rrx2linest  45976  aacllem  46391