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  3178  mob2  3686  reuind  3724  reupick3  4293  elpwunsn  4648  disjiun  5095  sotr2  5580  wefrc  5632  relop  5814  predpoirr  6306  predfrirr  6307  fnun  6632  mpteqb  6987  tpres  7175  fconst5  7180  funfvima  7204  riotaeqimp  7370  dfwe2  7750  limuni3  7828  tfisi  7835  trom  7851  funcnvuni  7908  resf1ext2b  7911  f1oweALT  7951  frxp  8105  poxp  8107  poxp2  8122  poxp3  8129  wfr3g  8298  onfununi  8310  tz7.48lem  8409  oecl  8501  oaordex  8522  oaass  8525  omwordri  8536  odi  8543  omass  8544  omeu  8549  oen0  8550  oewordi  8555  oewordri  8556  nnarcl  8580  nnmass  8588  brinxper  8700  findcard2  9128  rex2dom  9193  dif1ennnALT  9222  unblem1  9239  unblem2  9240  domunfican  9272  marypha1lem  9384  supiso  9427  inf3lem3  9583  epfrs  9684  frr3g  9709  karden  9848  infxpenlem  9966  iunfictbso  10067  dfac5  10082  dfac2b  10084  kmlem1  10104  kmlem9  10112  infpssrlem3  10258  fin23lem25  10277  fin23lem30  10295  domtriomlem  10395  axdc3lem4  10406  axcclem  10410  zorn2lem7  10455  konigthlem  10521  wunr1om  10672  tskr1om  10720  gruen  10765  grur1a  10772  indpi  10860  genpnmax  10960  prlem934  10986  ltaddpr  10987  ltexprlem7  10995  ltaprlem  10997  axrrecex  11116  axpre-sup  11122  lelttr  11264  dedekind  11337  addlid  11357  nn0lt2  12597  fzind  12632  fnn0ind  12633  btwnz  12637  uzwo  12870  lbzbi  12895  rpnnen1lem5  12940  ledivge1le  13024  xrlelttr  13116  qbtwnre  13159  xrsupsslem  13267  xrinfmsslem  13268  supxrun  13276  elfz1b  13554  elfz0ubfz0  13593  elfzo0z  13662  fzofzim  13670  elfznelfzo  13733  fleqceilz  13816  fsequb  13940  leexp2r  14139  bernneq  14194  fi1uzind  14472  brfi1indALT  14475  swrdnd0  14622  swrdswrdlem  14669  swrdswrd  14670  wrd2ind  14688  swrdccatin1  14690  swrdccatin2  14694  pfxccatin12lem3  14697  repswswrd  14749  cshweqrep  14786  swrd2lsw  14918  2swrd2eqwrdeq  14919  wrdl3s3  14928  s3iunsndisj  14934  cau3lem  15321  climuni  15518  mulcn2  15562  dvdsabseq  16283  divalglem8  16370  ndvdssub  16379  rplpwr  16528  algcvgblem  16547  lcmf  16603  lcmftp  16606  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfdvdsb  16613  lcmfun  16615  euclemma  16683  prmlem1a  17077  setsstruct2  17144  iscatd  17634  initoeu1  17973  initoeu2  17978  termoeu1  17980  plelttr  18303  insubm  18745  grpinveu  18906  cyccom  19135  symgfixelsi  19365  efgred  19678  telgsumfzs  19919  srgmulgass  20126  srgbinom  20140  lspdisjb  21036  mplcoe5lem  21946  cply1mul  22183  coe1fzgsumd  22191  gsummoncoe1  22195  evl1gsumd  22244  cpmatacl  22603  cpmatmcllem  22605  basis2  22838  0ntr  22958  uncmp  23290  1stcrest  23340  txcls  23491  txcnp  23507  tx1stc  23537  fgss2  23761  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  metcnp3  24428  tngngp3  24544  reconn  24717  iscau4  25179  ellimc3  25780  ulmbdd  26307  ulmcn  26308  sinq12ge0  26417  gausslemma2dlem3  27279  2sq2  27344  2sqreultlem  27358  2sqreunnltlem  27361  ssltleft  27782  ssltright  27783  noseqind  28186  expsgt0  28322  ax5seglem5  28860  ax5seg  28865  uhgrnbgr0nb  29281  cplgrop  29364  wlkl1loop  29566  uspgr2wlkeq  29574  upgrwlkdvdelem  29666  uhgrwkspthlem2  29684  pthdlem2lem  29697  uspgrn2crct  29738  wlkiswwlks2lem3  29801  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wwlksnext  29823  wwlksnextfun  29828  rusgrnumwwlk  29905  clwlkclwwlklem2a4  29926  clwlkclwwlklem3  29930  erclwwlksym  29950  erclwwlknsym  29999  eleclclwwlkn  30005  clwwlknonwwlknonb  30035  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  conngrv2edg  30124  eupth2lem3lem6  30162  frgrncvvdeqlem8  30235  frgrwopreglem4a  30239  frgrreggt1  30322  frgrreg  30323  grpoinveu  30448  ococss  31222  shmodsi  31318  h1datomi  31510  hoaddsub  31745  adjmul  32021  chjatom  32286  atomli  32311  atcvat4i  32326  mdsymlem3  32334  mdsymlem5  32336  mdsymlem6  32337  sumdmdlem  32347  cdj3lem2a  32365  cdj3lem3a  32368  bnj1204  35002  umgr2cycllem  35127  umgr2cycl  35128  cvmsdisj  35257  satfv0fun  35358  satffunlem  35388  satffunlem1lem2  35390  satffunlem2lem2  35393  fundmpss  35754  dfon2lem6  35776  dfon2lem8  35778  ifscgr  36032  lineext  36064  fscgr  36068  idinside  36072  btwnconn1lem11  36085  btwnconn1lem12  36086  btwnconn3  36091  brsegle  36096  seglecgr12  36099  hilbert1.2  36143  exp5d  36290  exp5k  36292  nn0prpwlem  36310  bj-restb  37082  exrecfnlem  37367  poimirlem26  37640  poimirlem29  37643  poimirlem32  37646  areacirc  37707  heibor1lem  37803  pridl  38031  pridlc  38065  dmnnzd  38069  disjlem17  38791  membpartlem19  38803  prtlem11  38859  prtlem17  38869  ax12indn  38936  atcvrj0  39422  cvrat4  39437  athgt  39450  lplnexllnN  39558  2llnjN  39561  lvolnle3at  39576  lncmp  39777  paddclN  39836  pexmidlem4N  39967  cdleme17d3  40490  cdleme50trn2  40545  cdlemf2  40556  cdlemf  40557  cdlemj3  40817  cdlemk26b-3  40899  dihord5b  41253  isnacs3  42698  jm2.26  42991  ordnexbtwnsuc  43256  omabs2  43321  naddgeoa  43383  sbiota1  44423  exbir  44469  tratrb  44526  onfrALT  44539  in2an  44598  pwtrrVD  44814  suctrALT2VD  44825  suctrALT2  44826  tratrbVD  44850  trintALTVD  44869  trintALT  44870  or2expropbi  47035  fcoresf1  47070  2reu8i  47114  2reuimp  47116  zm1nn  47303  2ffzoeq  47328  iccpartiltu  47423  iccpartigtl  47424  iccpartgt  47428  iccpartnel  47439  sbcpr  47522  fmtnofac2lem  47569  fmtnofac2  47570  lighneallem2  47607  odd2prm2  47719  stgoldbwt  47777  sbgoldbst  47779  sbgoldbaltlem1  47780  mogoldbb  47786  uhgrimisgrgric  47931  clnbgrgrim  47934  grimedg  47935  gpgedgvtx1  48053  gpgedg2iv  48058  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  lidldomn1  48219  ply1mulgsumlem1  48375  lincsumcl  48420  ellcoellss  48424  islinindfis  48438  lindslinindsimp1  48446  lindslinindsimp2lem5  48451  lindsrng01  48457  elfzolborelfzop1  48508  rrx2linest  48731  aacllem  49790