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 206  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  603  mpan2d  692  a2and  843  3impib  1116  exp5o  1355  ralrimivv  3197  mob2  3707  reuind  3745  reupick3  4315  elpwunsn  4680  disjiun  5128  sotr2  5613  wefrc  5663  relop  5842  predpoirr  6323  predfrirr  6324  fnun  6650  mpteqb  7003  tpres  7186  fconst5  7191  funfvima  7216  riotaeqimp  7376  dfwe2  7744  limuni3  7824  tfisi  7831  trom  7847  funcnvuni  7904  f1oweALT  7941  frxp  8094  poxp  8096  poxp2  8111  poxp3  8118  wfr3g  8289  wfrlem12OLD  8302  onfununi  8323  tz7.48lem  8423  oecl  8519  oaordex  8541  oaass  8544  omwordri  8555  odi  8562  omass  8563  omeu  8568  oen0  8569  oewordi  8574  oewordri  8575  nnarcl  8599  nnmass  8607  findcard2  9147  rex2dom  9229  dif1ennnALT  9260  findcard2OLD  9267  unblem1  9278  unblem2  9279  domunfican  9303  marypha1lem  9410  supiso  9452  inf3lem3  9607  epfrs  9708  frr3g  9733  karden  9872  infxpenlem  9990  iunfictbso  10091  dfac5  10105  dfac2b  10107  kmlem1  10127  kmlem9  10135  infpssrlem3  10282  fin23lem25  10301  fin23lem30  10319  domtriomlem  10419  axdc3lem4  10430  axcclem  10434  zorn2lem7  10479  konigthlem  10545  wunr1om  10696  tskr1om  10744  gruen  10789  grur1a  10796  indpi  10884  genpnmax  10984  prlem934  11010  ltaddpr  11011  ltexprlem7  11019  ltaprlem  11021  axrrecex  11140  axpre-sup  11146  lelttr  11286  dedekind  11359  addlid  11379  nn0lt2  12607  fzind  12642  fnn0ind  12643  btwnz  12647  uzwo  12877  lbzbi  12902  rpnnen1lem5  12947  ledivge1le  13027  xrlelttr  13117  qbtwnre  13160  xrsupsslem  13268  xrinfmsslem  13269  supxrun  13277  elfz1b  13552  elfz0ubfz0  13587  elfzo0z  13656  fzofzim  13661  elfznelfzo  13719  fleqceilz  13801  fsequb  13922  leexp2r  14121  bernneq  14174  fi1uzind  14440  brfi1indALT  14443  swrdnd0  14589  swrdswrdlem  14636  swrdswrd  14637  wrd2ind  14655  swrdccatin1  14657  swrdccatin2  14661  pfxccatin12lem3  14664  repswswrd  14716  cshweqrep  14753  swrd2lsw  14885  2swrd2eqwrdeq  14886  wrdl3s3  14895  s3iunsndisj  14897  cau3lem  15283  climuni  15478  mulcn2  15522  dvdsabseq  16238  divalglem8  16325  ndvdssub  16334  rplpwr  16481  algcvgblem  16496  lcmf  16552  lcmftp  16555  lcmfunsnlem2lem1  16557  lcmfunsnlem2lem2  16558  lcmfdvdsb  16562  lcmfun  16564  euclemma  16632  prmlem1a  17022  setsstruct2  17089  iscatd  17599  initoeu1  17943  initoeu2  17948  termoeu1  17950  plelttr  18279  insubm  18675  grpinveu  18834  cyccom  19046  symgfixelsi  19267  efgred  19580  telgsumfzs  19816  srgmulgass  19998  srgbinom  20012  lspdisjb  20688  mplcoe5lem  21522  cply1mul  21747  coe1fzgsumd  21755  gsummoncoe1  21757  evl1gsumd  21805  cpmatacl  22147  cpmatmcllem  22149  basis2  22383  0ntr  22504  uncmp  22836  1stcrest  22886  txcls  23037  txcnp  23053  tx1stc  23083  fgss2  23307  alexsubALTlem2  23481  alexsubALTlem3  23482  alexsubALTlem4  23483  metcnp3  23978  tngngp3  24102  reconn  24273  iscau4  24725  ellimc3  25325  ulmbdd  25839  ulmcn  25840  sinq12ge0  25947  gausslemma2dlem3  26798  2sq2  26863  2sqreultlem  26877  2sqreunnltlem  26880  ssltleft  27288  ssltright  27289  ax5seglem5  28056  ax5seg  28061  uhgrnbgr0nb  28476  cplgrop  28559  wlkl1loop  28760  uspgr2wlkeq  28768  upgrwlkdvdelem  28858  uhgrwkspthlem2  28876  pthdlem2lem  28889  uspgrn2crct  28927  wlkiswwlks2lem3  28990  wlkiswwlks2  28994  wlkiswwlksupgr2  28996  wlklnwwlkln2lem  29001  wwlksnext  29012  wwlksnextfun  29017  rusgrnumwwlk  29094  clwlkclwwlklem2a4  29115  clwlkclwwlklem3  29119  erclwwlksym  29139  erclwwlknsym  29188  eleclclwwlkn  29194  clwwlknonwwlknonb  29224  upgr3v3e3cycl  29298  upgr4cycl4dv4e  29303  conngrv2edg  29313  eupth2lem3lem6  29351  frgrncvvdeqlem8  29424  frgrwopreglem4a  29428  frgrreggt1  29511  frgrreg  29512  grpoinveu  29635  ococss  30409  shmodsi  30505  h1datomi  30697  hoaddsub  30932  adjmul  31208  chjatom  31473  atomli  31498  atcvat4i  31513  mdsymlem3  31521  mdsymlem5  31523  mdsymlem6  31524  sumdmdlem  31534  cdj3lem2a  31552  cdj3lem3a  31555  bnj1204  33852  umgr2cycllem  33960  umgr2cycl  33961  cvmsdisj  34090  satfv0fun  34191  satffunlem  34221  satffunlem1lem2  34223  satffunlem2lem2  34226  fundmpss  34566  dfon2lem6  34588  dfon2lem8  34590  ifscgr  34844  lineext  34876  fscgr  34880  idinside  34884  btwnconn1lem11  34897  btwnconn1lem12  34898  btwnconn3  34903  brsegle  34908  seglecgr12  34911  hilbert1.2  34955  exp5d  34989  exp5k  34991  nn0prpwlem  35009  bj-restb  35777  exrecfnlem  36062  poimirlem26  36316  poimirlem29  36319  poimirlem32  36322  areacirc  36383  heibor1lem  36480  pridl  36708  pridlc  36742  dmnnzd  36746  disjlem17  37472  membpartlem19  37484  prtlem11  37539  prtlem17  37549  ax12indn  37616  atcvrj0  38102  cvrat4  38117  athgt  38130  lplnexllnN  38238  2llnjN  38241  lvolnle3at  38256  lncmp  38457  paddclN  38516  pexmidlem4N  38647  cdleme17d3  39170  cdleme50trn2  39225  cdlemf2  39236  cdlemf  39237  cdlemj3  39497  cdlemk26b-3  39579  dihord5b  39933  isnacs3  41217  jm2.26  41510  ordnexbtwnsuc  41786  omabs2  41851  naddgeoa  41914  sbiota1  42962  exbir  43008  tratrb  43066  onfrALT  43079  in2an  43138  pwtrrVD  43355  suctrALT2VD  43366  suctrALT2  43367  tratrbVD  43391  trintALTVD  43410  trintALT  43411  or2expropbi  45514  fcoresf1  45549  2reu8i  45591  2reuimp  45593  zm1nn  45780  2ffzoeq  45806  iccpartiltu  45860  iccpartigtl  45861  iccpartgt  45865  iccpartnel  45876  sbcpr  45959  fmtnofac2lem  46006  fmtnofac2  46007  lighneallem2  46044  odd2prm2  46156  stgoldbwt  46214  sbgoldbst  46216  sbgoldbaltlem1  46217  mogoldbb  46223  isomuspgrlem1  46265  isomuspgrlem2d  46269  lidldomn1  46465  ply1mulgsumlem1  46713  lincsumcl  46758  ellcoellss  46762  islinindfis  46776  lindslinindsimp1  46784  lindslinindsimp2lem5  46789  lindsrng01  46795  elfzolborelfzop1  46846  rrx2linest  47074  aacllem  47494