Theorem expd 416

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  expcomd  417  exp32  421  exp4b  431  exp4c  433  exp4d  434  exp42  436  exp44  438  exp5c  445  exp5j  446  exp5l  447  pm3.3  449  expdimp  453  impl  456  syland  609  mpan2d  700  a2and  851  3impib  1122  exp5o  1362  ralrimivv  3181  mob2  3663  reuind  3701  reupick3  4265  elpwunsn  4623  disjiun  5067  sotr2  5567  wefrc  5619  relop  5799  predpoirr  6291  predfrirr  6292  fnun  6606  mpteqb  6962  tpres  7152  fconst5  7157  funfvima  7181  riotaeqimp  7346  dfwe2  7724  limuni3  7799  tfisi  7806  trom  7822  funcnvuni  7879  resf1ext2b  7882  f1oweALT  7921  frxp  8073  poxp  8075  poxp2  8090  poxp3  8097  wfr3g  8266  onfununi  8278  tz7.48lem  8377  oecl  8469  oaordex  8490  oaass  8493  omwordri  8504  odi  8511  omass  8512  omeu  8517  oen0  8519  oewordi  8524  oewordri  8525  nnarcl  8549  nnmass  8557  brinxper  8670  findcard2  9096  rex2dom  9160  dif1ennnALT  9184  unblem1  9199  unblem2  9200  domunfican  9229  marypha1lem  9343  supiso  9386  inf3lem3  9549  epfrs  9650  frr3g  9678  karden  9817  infxpenlem  9933  iunfictbso  10034  dfac5  10049  dfac2b  10051  kmlem1  10071  kmlem9  10079  infpssrlem3  10225  fin23lem25  10244  fin23lem30  10262  domtriomlem  10362  axdc3lem4  10373  axcclem  10377  zorn2lem7  10422  konigthlem  10489  wunr1om  10640  tskr1om  10688  gruen  10733  grur1a  10740  indpi  10828  genpnmax  10928  prlem934  10954  ltaddpr  10955  ltexprlem7  10963  ltaprlem  10965  axrrecex  11084  axpre-sup  11090  lelttr  11234  dedekind  11307  addlid  11327  nn0lt2  12590  fzind  12625  fnn0ind  12626  btwnz  12630  uzwo  12859  lbzbi  12884  rpnnen1lem5  12929  ledivge1le  13013  xrlelttr  13105  qbtwnre  13149  xrsupsslem  13257  xrinfmsslem  13258  supxrun  13266  elfz1b  13545  elfz0ubfz0  13584  elfzo0z  13654  fzofzim  13662  elfznelfzo  13726  fleqceilz  13811  fsequb  13935  leexp2r  14134  bernneq  14189  fi1uzind  14467  brfi1indALT  14470  swrdnd0  14618  swrdswrdlem  14664  swrdswrd  14665  wrd2ind  14683  swrdccatin1  14685  swrdccatin2  14689  pfxccatin12lem3  14692  repswswrd  14744  cshweqrep  14781  swrd2lsw  14912  2swrd2eqwrdeq  14913  wrdl3s3  14922  s3iunsndisj  14928  cau3lem  15315  climuni  15512  mulcn2  15556  dvdsabseq  16280  divalglem8  16367  ndvdssub  16376  rplpwr  16525  algcvgblem  16544  lcmf  16600  lcmftp  16603  lcmfunsnlem2lem1  16605  lcmfunsnlem2lem2  16606  lcmfdvdsb  16610  lcmfun  16612  euclemma  16681  prmlem1a  17075  setsstruct2  17142  iscatd  17637  initoeu1  17976  initoeu2  17981  termoeu1  17983  plelttr  18306  insubm  18784  grpinveu  18948  cyccom  19176  symgfixelsi  19408  efgred  19721  telgsumfzs  19962  srgmulgass  20196  srgbinom  20210  lspdisjb  21126  mplcoe5lem  22022  cply1mul  22289  coe1fzgsumd  22297  gsummoncoe1  22301  evl1gsumd  22350  cpmatacl  22706  cpmatmcllem  22708  basis2  22941  0ntr  23061  uncmp  23393  1stcrest  23443  txcls  23594  txcnp  23610  tx1stc  23640  fgss2  23864  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  metcnp3  24530  tngngp3  24646  reconn  24819  iscau4  25271  ellimc3  25871  ulmbdd  26388  ulmcn  26389  sinq12ge0  26497  gausslemma2dlem3  27356  2sq2  27421  2sqreultlem  27435  2sqreunnltlem  27438  sltsleft  27877  sltsright  27878  noseqind  28309  oldfib  28394  expsgt0  28454  bdayfinbndlem1  28484  bdayfin  28504  elreno2  28512  ax5seglem5  29027  ax5seg  29032  uhgrnbgr0nb  29448  cplgrop  29531  wlkl1loop  29731  uspgr2wlkeq  29739  upgrwlkdvdelem  29829  uhgrwkspthlem2  29847  pthdlem2lem  29860  uspgrn2crct  29901  wlkiswwlks2lem3  29964  wlkiswwlks2  29968  wlkiswwlksupgr2  29970  wlklnwwlkln2lem  29975  wwlksnext  29986  wwlksnextfun  29991  rusgrnumwwlk  30071  clwlkclwwlklem2a4  30092  clwlkclwwlklem3  30096  erclwwlksym  30116  erclwwlknsym  30165  eleclclwwlkn  30171  clwwlknonwwlknonb  30201  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  conngrv2edg  30290  eupth2lem3lem6  30328  frgrncvvdeqlem8  30401  frgrwopreglem4a  30405  frgrreggt1  30488  frgrreg  30489  grpoinveu  30615  ococss  31389  shmodsi  31485  h1datomi  31677  hoaddsub  31912  adjmul  32188  chjatom  32453  atomli  32478  atcvat4i  32493  mdsymlem3  32501  mdsymlem5  32503  mdsymlem6  32504  sumdmdlem  32514  cdj3lem2a  32532  cdj3lem3a  32535  bnj1204  35201  fineqvinfep  35313  umgr2cycllem  35375  umgr2cycl  35376  cvmsdisj  35505  satfv0fun  35606  satffunlem  35636  satffunlem1lem2  35638  satffunlem2lem2  35641  fundmpss  36002  dfon2lem6  36021  dfon2lem8  36023  ifscgr  36279  lineext  36311  fscgr  36315  idinside  36319  btwnconn1lem11  36332  btwnconn1lem12  36333  btwnconn3  36338  brsegle  36343  seglecgr12  36346  hilbert1.2  36390  exp5d  36537  exp5k  36539  nn0prpwlem  36557  mh-inf3f1  36776  bj-restb  37459  exrecfnlem  37748  poimirlem26  38020  poimirlem29  38023  poimirlem32  38026  areacirc  38087  heibor1lem  38183  pridl  38411  pridlc  38445  dmnnzd  38449  disjlem17  39276  membpartlem19  39288  prtlem11  39365  prtlem17  39375  ax12indn  39442  atcvrj0  39927  cvrat4  39942  athgt  39955  lplnexllnN  40063  2llnjN  40066  lvolnle3at  40081  lncmp  40282  paddclN  40341  pexmidlem4N  40472  cdleme17d3  40995  cdleme50trn2  41050  cdlemf2  41061  cdlemf  41062  cdlemj3  41322  cdlemk26b-3  41404  dihord5b  41758  isnacs3  43166  jm2.26  43454  ordnexbtwnsuc  43719  omabs2  43784  naddgeoa  43846  sbiota1  44885  exbir  44930  tratrb  44987  onfrALT  45000  in2an  45059  pwtrrVD  45275  suctrALT2VD  45286  suctrALT2  45287  tratrbVD  45311  trintALTVD  45330  trintALT  45331  or2expropbi  47504  fcoresf1  47539  2reu8i  47583  2reuimp  47585  zm1nn  47772  2ffzoeq  47798  iccpartiltu  47904  iccpartigtl  47905  iccpartgt  47909  iccpartnel  47920  sbcpr  48003  fmtnofac2lem  48053  fmtnofac2  48054  lighneallem2  48091  odd2prm2  48216  stgoldbwt  48274  sbgoldbst  48276  sbgoldbaltlem1  48277  mogoldbb  48283  uhgrimisgrgric  48429  clnbgrgrim  48432  grimedg  48433  gpgedgvtx1  48560  gpgedg2iv  48565  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622  pgnbgreunbgr  48623  lidldomn1  48729  ply1mulgsumlem1  48884  lincsumcl  48929  ellcoellss  48933  islinindfis  48947  lindslinindsimp1  48955  lindslinindsimp2lem5  48960  lindsrng01  48966  elfzolborelfzop1  49017  rrx2linest  49240  aacllem  50298