Theorem expd 419

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  expcomd  420  exp32  424  exp4b  434  exp4c  436  exp4d  437  exp42  439  exp44  441  exp5c  448  exp5j  449  exp5l  450  pm3.3  452  expdimp  456  impl  459  syland  606  mpan2d  694  a2and  845  3impib  1118  exp5o  1357  ralrimivv  3101  mob2  3617  reuind  3655  reupick3  4220  elpwunsn  4585  disjiun  5026  sotr2  5485  wefrc  5530  relop  5704  predpoirr  6169  predfrirr  6170  fnun  6468  mpteqb  6815  tpres  6994  fconst5  6999  funfvima  7024  riotaeqimp  7175  dfwe2  7537  limuni3  7609  tfisi  7615  trom  7631  funcnvuni  7687  f1oweALT  7723  frxp  7871  poxp  7873  wfr3g  8031  wfrlem12  8044  onfununi  8056  tz7.48lem  8155  oecl  8242  oaordex  8264  oaass  8267  omwordri  8278  odi  8285  omass  8286  omeu  8291  oen0  8292  oewordi  8297  oewordri  8298  nnarcl  8322  nnmass  8330  findcard2  8820  dif1enOLD  8885  findcard2OLD  8891  unblem1  8901  unblem2  8902  domunfican  8922  marypha1lem  9027  supiso  9069  inf3lem3  9223  epfrs  9325  karden  9476  infxpenlem  9592  iunfictbso  9693  dfac5  9707  dfac2b  9709  kmlem1  9729  kmlem9  9737  infpssrlem3  9884  fin23lem25  9903  fin23lem30  9921  domtriomlem  10021  axdc3lem4  10032  axcclem  10036  zorn2lem7  10081  konigthlem  10147  wunr1om  10298  tskr1om  10346  gruen  10391  grur1a  10398  indpi  10486  genpnmax  10586  prlem934  10612  ltaddpr  10613  ltexprlem7  10621  ltaprlem  10623  axrrecex  10742  axpre-sup  10748  lelttr  10888  dedekind  10960  addid2  10980  nn0lt2  12205  fzind  12240  fnn0ind  12241  btwnz  12244  uzwo  12472  lbzbi  12497  rpnnen1lem5  12542  ledivge1le  12622  xrlelttr  12711  qbtwnre  12754  xrsupsslem  12862  xrinfmsslem  12863  supxrun  12871  elfz1b  13146  elfz0ubfz0  13181  elfzo0z  13249  fzofzim  13254  elfznelfzo  13312  fleqceilz  13392  fsequb  13513  leexp2r  13709  bernneq  13761  fi1uzind  14028  brfi1indALT  14031  swrdnd0  14187  swrdswrdlem  14234  swrdswrd  14235  wrd2ind  14253  swrdccatin1  14255  swrdccatin2  14259  pfxccatin12lem3  14262  repswswrd  14314  cshweqrep  14351  swrd2lsw  14482  2swrd2eqwrdeq  14483  wrdl3s3  14494  s3iunsndisj  14496  cau3lem  14883  climuni  15078  mulcn2  15122  dvdsabseq  15837  divalglem8  15924  ndvdssub  15933  rplpwr  16082  algcvgblem  16097  lcmf  16153  lcmftp  16156  lcmfunsnlem2lem1  16158  lcmfunsnlem2lem2  16159  lcmfdvdsb  16163  lcmfun  16165  euclemma  16233  prmlem1a  16623  setsstruct2  16703  iscatd  17130  initoeu1  17471  initoeu2  17476  termoeu1  17478  plelttr  17804  insubm  18199  grpinveu  18356  cyccom  18564  symgfixelsi  18781  efgred  19092  telgsumfzs  19328  srgmulgass  19500  srgbinom  19514  lspdisjb  20117  mplcoe5lem  20950  cply1mul  21169  coe1fzgsumd  21177  gsummoncoe1  21179  evl1gsumd  21227  cpmatacl  21567  cpmatmcllem  21569  basis2  21802  0ntr  21922  uncmp  22254  1stcrest  22304  txcls  22455  txcnp  22471  tx1stc  22501  fgss2  22725  alexsubALTlem2  22899  alexsubALTlem3  22900  alexsubALTlem4  22901  metcnp3  23392  tngngp3  23508  reconn  23679  iscau4  24130  ellimc3  24730  ulmbdd  25244  ulmcn  25245  sinq12ge0  25352  gausslemma2dlem3  26203  2sq2  26268  2sqreultlem  26282  2sqreunnltlem  26285  ax5seglem5  26978  ax5seg  26983  uhgrnbgr0nb  27396  cplgrop  27479  wlkl1loop  27679  uspgr2wlkeq  27687  upgrwlkdvdelem  27777  uhgrwkspthlem2  27795  pthdlem2lem  27808  uspgrn2crct  27846  wlkiswwlks2lem3  27909  wlkiswwlks2  27913  wlkiswwlksupgr2  27915  wlklnwwlkln2lem  27920  wwlksnext  27931  wwlksnextfun  27936  rusgrnumwwlk  28013  clwlkclwwlklem2a4  28034  clwlkclwwlklem3  28038  erclwwlksym  28058  erclwwlknsym  28107  eleclclwwlkn  28113  clwwlknonwwlknonb  28143  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  conngrv2edg  28232  eupth2lem3lem6  28270  frgrncvvdeqlem8  28343  frgrwopreglem4a  28347  frgrreggt1  28430  frgrreg  28431  grpoinveu  28554  ococss  29328  shmodsi  29424  h1datomi  29616  hoaddsub  29851  adjmul  30127  chjatom  30392  atomli  30417  atcvat4i  30432  mdsymlem3  30440  mdsymlem5  30442  mdsymlem6  30443  sumdmdlem  30453  cdj3lem2a  30471  cdj3lem3a  30474  bnj1204  32659  umgr2cycllem  32769  umgr2cycl  32770  cvmsdisj  32899  satfv0fun  33000  satffunlem  33030  satffunlem1lem2  33032  satffunlem2lem2  33035  fundmpss  33410  dfon2lem6  33434  dfon2lem8  33436  poxp2  33470  poxp3  33476  frr3g  33504  ssltleft  33740  ssltright  33741  ifscgr  34032  lineext  34064  fscgr  34068  idinside  34072  btwnconn1lem11  34085  btwnconn1lem12  34086  btwnconn3  34091  brsegle  34096  seglecgr12  34099  hilbert1.2  34143  exp5d  34177  exp5k  34179  nn0prpwlem  34197  bj-restb  34949  exrecfnlem  35236  poimirlem26  35489  poimirlem29  35492  poimirlem32  35495  areacirc  35556  heibor1lem  35653  pridl  35881  pridlc  35915  dmnnzd  35919  prtlem11  36566  prtlem17  36576  ax12indn  36643  atcvrj0  37128  cvrat4  37143  athgt  37156  lplnexllnN  37264  2llnjN  37267  lvolnle3at  37282  lncmp  37483  paddclN  37542  pexmidlem4N  37673  cdleme17d3  38196  cdleme50trn2  38251  cdlemf2  38262  cdlemf  38263  cdlemj3  38523  cdlemk26b-3  38605  dihord5b  38959  isnacs3  40176  jm2.26  40468  sbiota1  41666  exbir  41712  tratrb  41770  onfrALT  41783  in2an  41842  pwtrrVD  42059  suctrALT2VD  42070  suctrALT2  42071  tratrbVD  42095  trintALTVD  42114  trintALT  42115  or2expropbi  44143  fcoresf1  44178  2reu8i  44220  2reuimp  44222  zm1nn  44410  2ffzoeq  44436  iccpartiltu  44490  iccpartigtl  44491  iccpartgt  44495  iccpartnel  44506  sbcpr  44589  fmtnofac2lem  44636  fmtnofac2  44637  lighneallem2  44674  odd2prm2  44786  stgoldbwt  44844  sbgoldbst  44846  sbgoldbaltlem1  44847  mogoldbb  44853  isomuspgrlem1  44895  isomuspgrlem2d  44899  lidldomn1  45095  ply1mulgsumlem1  45343  lincsumcl  45388  ellcoellss  45392  islinindfis  45406  lindslinindsimp1  45414  lindslinindsimp2lem5  45419  lindsrng01  45425  elfzolborelfzop1  45476  rrx2linest  45704  aacllem  46119