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  3179  mob2  3689  reuind  3727  reupick3  4296  elpwunsn  4651  disjiun  5098  sotr2  5583  wefrc  5635  relop  5817  predpoirr  6309  predfrirr  6310  fnun  6635  mpteqb  6990  tpres  7178  fconst5  7183  funfvima  7207  riotaeqimp  7373  dfwe2  7753  limuni3  7831  tfisi  7838  trom  7854  funcnvuni  7911  resf1ext2b  7914  f1oweALT  7954  frxp  8108  poxp  8110  poxp2  8125  poxp3  8132  wfr3g  8301  onfununi  8313  tz7.48lem  8412  oecl  8504  oaordex  8525  oaass  8528  omwordri  8539  odi  8546  omass  8547  omeu  8552  oen0  8553  oewordi  8558  oewordri  8559  nnarcl  8583  nnmass  8591  brinxper  8703  findcard2  9134  rex2dom  9200  dif1ennnALT  9229  unblem1  9246  unblem2  9247  domunfican  9279  marypha1lem  9391  supiso  9434  inf3lem3  9590  epfrs  9691  frr3g  9716  karden  9855  infxpenlem  9973  iunfictbso  10074  dfac5  10089  dfac2b  10091  kmlem1  10111  kmlem9  10119  infpssrlem3  10265  fin23lem25  10284  fin23lem30  10302  domtriomlem  10402  axdc3lem4  10413  axcclem  10417  zorn2lem7  10462  konigthlem  10528  wunr1om  10679  tskr1om  10727  gruen  10772  grur1a  10779  indpi  10867  genpnmax  10967  prlem934  10993  ltaddpr  10994  ltexprlem7  11002  ltaprlem  11004  axrrecex  11123  axpre-sup  11129  lelttr  11271  dedekind  11344  addlid  11364  nn0lt2  12604  fzind  12639  fnn0ind  12640  btwnz  12644  uzwo  12877  lbzbi  12902  rpnnen1lem5  12947  ledivge1le  13031  xrlelttr  13123  qbtwnre  13166  xrsupsslem  13274  xrinfmsslem  13275  supxrun  13283  elfz1b  13561  elfz0ubfz0  13600  elfzo0z  13669  fzofzim  13677  elfznelfzo  13740  fleqceilz  13823  fsequb  13947  leexp2r  14146  bernneq  14201  fi1uzind  14479  brfi1indALT  14482  swrdnd0  14629  swrdswrdlem  14676  swrdswrd  14677  wrd2ind  14695  swrdccatin1  14697  swrdccatin2  14701  pfxccatin12lem3  14704  repswswrd  14756  cshweqrep  14793  swrd2lsw  14925  2swrd2eqwrdeq  14926  wrdl3s3  14935  s3iunsndisj  14941  cau3lem  15328  climuni  15525  mulcn2  15569  dvdsabseq  16290  divalglem8  16377  ndvdssub  16386  rplpwr  16535  algcvgblem  16554  lcmf  16610  lcmftp  16613  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfdvdsb  16620  lcmfun  16622  euclemma  16690  prmlem1a  17084  setsstruct2  17151  iscatd  17641  initoeu1  17980  initoeu2  17985  termoeu1  17987  plelttr  18310  insubm  18752  grpinveu  18913  cyccom  19142  symgfixelsi  19372  efgred  19685  telgsumfzs  19926  srgmulgass  20133  srgbinom  20147  lspdisjb  21043  mplcoe5lem  21953  cply1mul  22190  coe1fzgsumd  22198  gsummoncoe1  22202  evl1gsumd  22251  cpmatacl  22610  cpmatmcllem  22612  basis2  22845  0ntr  22965  uncmp  23297  1stcrest  23347  txcls  23498  txcnp  23514  tx1stc  23544  fgss2  23768  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  metcnp3  24435  tngngp3  24551  reconn  24724  iscau4  25186  ellimc3  25787  ulmbdd  26314  ulmcn  26315  sinq12ge0  26424  gausslemma2dlem3  27286  2sq2  27351  2sqreultlem  27365  2sqreunnltlem  27368  ssltleft  27789  ssltright  27790  noseqind  28193  expsgt0  28329  ax5seglem5  28867  ax5seg  28872  uhgrnbgr0nb  29288  cplgrop  29371  wlkl1loop  29573  uspgr2wlkeq  29581  upgrwlkdvdelem  29673  uhgrwkspthlem2  29691  pthdlem2lem  29704  uspgrn2crct  29745  wlkiswwlks2lem3  29808  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wlklnwwlkln2lem  29819  wwlksnext  29830  wwlksnextfun  29835  rusgrnumwwlk  29912  clwlkclwwlklem2a4  29933  clwlkclwwlklem3  29937  erclwwlksym  29957  erclwwlknsym  30006  eleclclwwlkn  30012  clwwlknonwwlknonb  30042  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  conngrv2edg  30131  eupth2lem3lem6  30169  frgrncvvdeqlem8  30242  frgrwopreglem4a  30246  frgrreggt1  30329  frgrreg  30330  grpoinveu  30455  ococss  31229  shmodsi  31325  h1datomi  31517  hoaddsub  31752  adjmul  32028  chjatom  32293  atomli  32318  atcvat4i  32333  mdsymlem3  32341  mdsymlem5  32343  mdsymlem6  32344  sumdmdlem  32354  cdj3lem2a  32372  cdj3lem3a  32375  bnj1204  35009  umgr2cycllem  35134  umgr2cycl  35135  cvmsdisj  35264  satfv0fun  35365  satffunlem  35395  satffunlem1lem2  35397  satffunlem2lem2  35400  fundmpss  35761  dfon2lem6  35783  dfon2lem8  35785  ifscgr  36039  lineext  36071  fscgr  36075  idinside  36079  btwnconn1lem11  36092  btwnconn1lem12  36093  btwnconn3  36098  brsegle  36103  seglecgr12  36106  hilbert1.2  36150  exp5d  36297  exp5k  36299  nn0prpwlem  36317  bj-restb  37089  exrecfnlem  37374  poimirlem26  37647  poimirlem29  37650  poimirlem32  37653  areacirc  37714  heibor1lem  37810  pridl  38038  pridlc  38072  dmnnzd  38076  disjlem17  38798  membpartlem19  38810  prtlem11  38866  prtlem17  38876  ax12indn  38943  atcvrj0  39429  cvrat4  39444  athgt  39457  lplnexllnN  39565  2llnjN  39568  lvolnle3at  39583  lncmp  39784  paddclN  39843  pexmidlem4N  39974  cdleme17d3  40497  cdleme50trn2  40552  cdlemf2  40563  cdlemf  40564  cdlemj3  40824  cdlemk26b-3  40906  dihord5b  41260  isnacs3  42705  jm2.26  42998  ordnexbtwnsuc  43263  omabs2  43328  naddgeoa  43390  sbiota1  44430  exbir  44476  tratrb  44533  onfrALT  44546  in2an  44605  pwtrrVD  44821  suctrALT2VD  44832  suctrALT2  44833  tratrbVD  44857  trintALTVD  44876  trintALT  44877  or2expropbi  47039  fcoresf1  47074  2reu8i  47118  2reuimp  47120  zm1nn  47307  2ffzoeq  47332  iccpartiltu  47427  iccpartigtl  47428  iccpartgt  47432  iccpartnel  47443  sbcpr  47526  fmtnofac2lem  47573  fmtnofac2  47574  lighneallem2  47611  odd2prm2  47723  stgoldbwt  47781  sbgoldbst  47783  sbgoldbaltlem1  47784  mogoldbb  47790  uhgrimisgrgric  47935  clnbgrgrim  47938  grimedg  47939  gpgedgvtx1  48057  gpgedg2iv  48062  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  lidldomn1  48223  ply1mulgsumlem1  48379  lincsumcl  48424  ellcoellss  48428  islinindfis  48442  lindslinindsimp1  48450  lindslinindsimp2lem5  48455  lindsrng01  48461  elfzolborelfzop1  48512  rrx2linest  48735  aacllem  49794