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  604  mpan2d  695  a2and  846  3impib  1117  exp5o  1357  ralrimivv  3179  mob2  3675  reuind  3713  reupick3  4284  elpwunsn  4643  disjiun  5088  sotr2  5574  wefrc  5626  relop  5807  predpoirr  6299  predfrirr  6300  fnun  6614  mpteqb  6969  tpres  7157  fconst5  7162  funfvima  7186  riotaeqimp  7351  dfwe2  7729  limuni3  7804  tfisi  7811  trom  7827  funcnvuni  7884  resf1ext2b  7887  f1oweALT  7926  frxp  8078  poxp  8080  poxp2  8095  poxp3  8102  wfr3g  8271  onfununi  8283  tz7.48lem  8382  oecl  8474  oaordex  8495  oaass  8498  omwordri  8509  odi  8516  omass  8517  omeu  8522  oen0  8524  oewordi  8529  oewordri  8530  nnarcl  8554  nnmass  8562  brinxper  8675  findcard2  9101  rex2dom  9165  dif1ennnALT  9189  unblem1  9204  unblem2  9205  domunfican  9234  marypha1lem  9348  supiso  9391  inf3lem3  9551  epfrs  9652  frr3g  9680  karden  9819  infxpenlem  9935  iunfictbso  10036  dfac5  10051  dfac2b  10053  kmlem1  10073  kmlem9  10081  infpssrlem3  10227  fin23lem25  10246  fin23lem30  10264  domtriomlem  10364  axdc3lem4  10375  axcclem  10379  zorn2lem7  10424  konigthlem  10491  wunr1om  10642  tskr1om  10690  gruen  10735  grur1a  10742  indpi  10830  genpnmax  10930  prlem934  10956  ltaddpr  10957  ltexprlem7  10965  ltaprlem  10967  axrrecex  11086  axpre-sup  11092  lelttr  11235  dedekind  11308  addlid  11328  nn0lt2  12567  fzind  12602  fnn0ind  12603  btwnz  12607  uzwo  12836  lbzbi  12861  rpnnen1lem5  12906  ledivge1le  12990  xrlelttr  13082  qbtwnre  13126  xrsupsslem  13234  xrinfmsslem  13235  supxrun  13243  elfz1b  13521  elfz0ubfz0  13560  elfzo0z  13629  fzofzim  13637  elfznelfzo  13701  fleqceilz  13786  fsequb  13910  leexp2r  14109  bernneq  14164  fi1uzind  14442  brfi1indALT  14445  swrdnd0  14593  swrdswrdlem  14639  swrdswrd  14640  wrd2ind  14658  swrdccatin1  14660  swrdccatin2  14664  pfxccatin12lem3  14667  repswswrd  14719  cshweqrep  14756  swrd2lsw  14887  2swrd2eqwrdeq  14888  wrdl3s3  14897  s3iunsndisj  14903  cau3lem  15290  climuni  15487  mulcn2  15531  dvdsabseq  16252  divalglem8  16339  ndvdssub  16348  rplpwr  16497  algcvgblem  16516  lcmf  16572  lcmftp  16575  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfdvdsb  16582  lcmfun  16584  euclemma  16652  prmlem1a  17046  setsstruct2  17113  iscatd  17608  initoeu1  17947  initoeu2  17952  termoeu1  17954  plelttr  18277  insubm  18755  grpinveu  18916  cyccom  19144  symgfixelsi  19376  efgred  19689  telgsumfzs  19930  srgmulgass  20164  srgbinom  20178  lspdisjb  21093  mplcoe5lem  22006  cply1mul  22252  coe1fzgsumd  22260  gsummoncoe1  22264  evl1gsumd  22313  cpmatacl  22672  cpmatmcllem  22674  basis2  22907  0ntr  23027  uncmp  23359  1stcrest  23409  txcls  23560  txcnp  23576  tx1stc  23606  fgss2  23830  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  metcnp3  24496  tngngp3  24612  reconn  24785  iscau4  25247  ellimc3  25848  ulmbdd  26375  ulmcn  26376  sinq12ge0  26485  gausslemma2dlem3  27347  2sq2  27412  2sqreultlem  27426  2sqreunnltlem  27429  sltsleft  27868  sltsright  27869  noseqind  28300  oldfib  28385  expsgt0  28445  bdayfinbndlem1  28475  bdayfin  28495  elreno2  28503  ax5seglem5  29018  ax5seg  29023  uhgrnbgr0nb  29439  cplgrop  29522  wlkl1loop  29723  uspgr2wlkeq  29731  upgrwlkdvdelem  29821  uhgrwkspthlem2  29839  pthdlem2lem  29852  uspgrn2crct  29893  wlkiswwlks2lem3  29956  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wwlksnext  29978  wwlksnextfun  29983  rusgrnumwwlk  30063  clwlkclwwlklem2a4  30084  clwlkclwwlklem3  30088  erclwwlksym  30108  erclwwlknsym  30157  eleclclwwlkn  30163  clwwlknonwwlknonb  30193  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  conngrv2edg  30282  eupth2lem3lem6  30320  frgrncvvdeqlem8  30393  frgrwopreglem4a  30397  frgrreggt1  30480  frgrreg  30481  grpoinveu  30606  ococss  31380  shmodsi  31476  h1datomi  31668  hoaddsub  31903  adjmul  32179  chjatom  32444  atomli  32469  atcvat4i  32484  mdsymlem3  32492  mdsymlem5  32494  mdsymlem6  32495  sumdmdlem  32505  cdj3lem2a  32523  cdj3lem3a  32526  bnj1204  35187  fineqvinfep  35300  umgr2cycllem  35353  umgr2cycl  35354  cvmsdisj  35483  satfv0fun  35584  satffunlem  35614  satffunlem1lem2  35616  satffunlem2lem2  35619  fundmpss  35980  dfon2lem6  35999  dfon2lem8  36001  ifscgr  36257  lineext  36289  fscgr  36293  idinside  36297  btwnconn1lem11  36310  btwnconn1lem12  36311  btwnconn3  36316  brsegle  36321  seglecgr12  36324  hilbert1.2  36368  exp5d  36515  exp5k  36517  nn0prpwlem  36535  bj-restb  37341  exrecfnlem  37628  poimirlem26  37891  poimirlem29  37894  poimirlem32  37897  areacirc  37958  heibor1lem  38054  pridl  38282  pridlc  38316  dmnnzd  38320  disjlem17  39147  membpartlem19  39159  prtlem11  39236  prtlem17  39246  ax12indn  39313  atcvrj0  39798  cvrat4  39813  athgt  39826  lplnexllnN  39934  2llnjN  39937  lvolnle3at  39952  lncmp  40153  paddclN  40212  pexmidlem4N  40343  cdleme17d3  40866  cdleme50trn2  40921  cdlemf2  40932  cdlemf  40933  cdlemj3  41193  cdlemk26b-3  41275  dihord5b  41629  isnacs3  43061  jm2.26  43353  ordnexbtwnsuc  43618  omabs2  43683  naddgeoa  43745  sbiota1  44784  exbir  44829  tratrb  44886  onfrALT  44899  in2an  44958  pwtrrVD  45174  suctrALT2VD  45185  suctrALT2  45186  tratrbVD  45210  trintALTVD  45229  trintALT  45230  or2expropbi  47388  fcoresf1  47423  2reu8i  47467  2reuimp  47469  zm1nn  47656  2ffzoeq  47681  iccpartiltu  47776  iccpartigtl  47777  iccpartgt  47781  iccpartnel  47792  sbcpr  47875  fmtnofac2lem  47922  fmtnofac2  47923  lighneallem2  47960  odd2prm2  48072  stgoldbwt  48130  sbgoldbst  48132  sbgoldbaltlem1  48133  mogoldbb  48139  uhgrimisgrgric  48285  clnbgrgrim  48288  grimedg  48289  gpgedgvtx1  48416  gpgedg2iv  48421  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem6  48478  pgnbgreunbgr  48479  lidldomn1  48585  ply1mulgsumlem1  48740  lincsumcl  48785  ellcoellss  48789  islinindfis  48803  lindslinindsimp1  48811  lindslinindsimp2lem5  48816  lindsrng01  48822  elfzolborelfzop1  48873  rrx2linest  49096  aacllem  50154