Theorem expd 421

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  expcomd  422  exp32  426  exp4b  436  exp4c  438  exp4d  439  exp42  441  exp44  443  exp5c  450  exp5j  451  exp5l  452  pm3.3  454  expdimp  458  impl  461  syland  615  mpan2d  707  a2and  859  3impib  1134  exp5o  1374  ralrimivv  3203  mob2  3672  reuind  3710  reupick3  4275  elpwunsn  4641  disjiun  5090  sotr2  5592  wefrc  5644  relop  5827  predpoirr  6336  predfrirr  6337  fnun  6653  mpteqb  7013  tpres  7207  fconst5  7212  funfvima  7236  riotaeqimp  7403  dfwe2  7788  limuni3  7863  tfisi  7870  trom  7886  funcnvuni  7944  resf1ext2b  7947  f1oweALT  7984  frxp  8140  poxp  8142  poxp2  8162  poxp3  8169  wfr3g  8340  onfununi  8352  tz7.48lemOLD  8454  oecl  8548  oaordex  8569  oaass  8572  omwordri  8583  odi  8590  omass  8591  omeu  8596  oen0  8598  oewordi  8603  oewordri  8604  nnarcl  8628  nnmass  8636  brinxper  8750  findcard2  9183  rex2dom  9247  dif1ennnALT  9271  unblem1  9287  unblem2  9288  domunfican  9316  marypha1lem  9428  supiso  9471  inf3lem3  9634  epfrs  9735  frr3g  9763  kardenOLD  9963  infxpenlem  10095  iunfictbso  10196  dfac5  10210  dfac2b  10212  kmlem1  10232  kmlem9  10240  infpssrlem3  10386  fin23lem25  10405  fin23lem30  10423  domtriomlem  10523  axdc3lem4  10534  axcclem  10538  zorn2lem7  10583  konigthlem  10656  wunr1om  10807  tskr1om  10855  gruen  10900  grur1a  10907  indpi  10995  genpnmax  11095  prlem934  11121  ltaddpr  11122  ltexprlem7  11130  ltaprlem  11132  axrrecex  11251  axpre-sup  11257  lelttr  11403  dedekind  11476  addlid  11496  nn0lt2  12765  fzind  12800  fnn0ind  12801  btwnz  12805  uzwo  13041  lbzbi  13066  rpnnen1lem5  13112  ledivge1le  13196  xrlelttr  13288  qbtwnre  13332  xrsupsslem  13440  xrinfmsslem  13441  supxrun  13449  elfz1b  13730  elfz0ubfz0  13769  elfzo0z  13839  fzofzim  13847  elfznelfzo  13911  fleqceilz  13997  fsequb  14121  leexp2r  14320  bernneq  14376  fi1uzind  14655  brfi1indALT  14658  swrdnd0  14811  swrdswrdlem  14857  swrdswrd  14858  wrd2ind  14876  swrdccatin1  14878  swrdccatin2  14882  pfxccatin12lem3  14885  repswswrd  14939  cshweqrep  14976  swrd2lsw  15110  2swrd2eqwrdeq  15111  wrdl3s3  15120  s3iunsndisj  15126  cau3lem  15527  climuni  15724  mulcn2  15768  dvdsabseq  16488  divalglem8  16575  ndvdssub  16584  rplpwr  16737  algcvgblem  16757  lcmf  16813  lcmftp  16816  lcmfunsnlem2lem1  16818  lcmfunsnlem2lem2  16819  lcmfdvdsb  16823  lcmfun  16825  euclemma  16894  prmlem1a  17289  setsstruct2  17357  iscatd  17852  initoeu1  18191  initoeu2  18196  termoeu1  18198  plelttr  18521  insubm  19019  grpinveu  19190  cyccom  19423  symgfixelsi  19654  efgred  19967  telgsumfzs  20208  srgmulgass  20448  srgbinom  20462  lspdisjb  21409  mplcoe5lem  22353  cply1mul  22619  coe1fzgsumd  22627  gsummoncoe1  22631  evl1gsumd  22680  cpmatacl  23039  cpmatmcllem  23041  basis2  23274  0ntr  23394  uncmp  23726  1stcrest  23776  txcls  23928  txcnp  23944  tx1stc  23974  fgss2  24198  alexsubALTlem2  24372  alexsubALTlem3  24373  alexsubALTlem4  24374  metcnp3  24864  tngngp3  24980  reconn  25153  iscau4  25605  ellimc3  26204  ulmbdd  26730  ulmcn  26731  sinq12ge0  26842  gausslemma2dlem3  27700  2sq2  27765  2sqreultlem  27779  2sqreunnltlem  27782  sltsleft  28251  sltsright  28252  noseqind  28683  oldfib  28768  expsgt0  28828  bdayfinbndlem1  28858  bdayfin  28878  elreno2  28886  ax5seglem5  29516  ax5seg  29521  uhgrnbgr0nb  29940  cplgrop  30023  wlkl1loop  30223  uspgr2wlkeq  30231  upgrwlkdvdelem  30327  uhgrwkspthlem2  30345  pthdlem2lem  30358  uspgrn2crct  30402  wlkiswwlks2lem3  30465  wlkiswwlks2  30469  wlkiswwlksupgr2  30471  wlklnwwlkln2lem  30476  wwlksnext  30487  wwlksnextfun  30492  rusgrnumwwlk  30572  clwlkclwwlklem2a4  30593  clwlkclwwlklem3  30597  erclwwlksym  30617  erclwwlknsym  30666  eleclclwwlkn  30672  clwwlknonwwlknonb  30702  umgr2cycllem  30751  umgr2cycl  30752  upgr3v3e3cycl  30786  upgr4cycl4dv4e  30791  conngrv2edg  30801  eupth2lem3lem6  30839  frgrncvvdeqlem8  30912  frgrwopreglem4a  30916  frgrreggt1  30999  frgrreg  31000  grpoinveu  31126  ococss  31900  shmodsi  31996  h1datomi  32188  hoaddsub  32423  adjmul  32699  chjatom  32964  atomli  32989  atcvat4i  33004  mdsymlem3  33012  mdsymlem5  33014  mdsymlem6  33015  sumdmdlem  33025  cdj3lem2a  33043  cdj3lem3a  33046  bnj1204  35688  rmo6  35756  fineqvinfep  35849  cvmsdisj  36121  satfv0fun  36222  satffunlem  36252  satffunlem1lem2  36254  satffunlem2lem2  36257  fundmpss  36624  dfon2lem6  36642  dfon2lem8  36644  ifscgr  36901  lineext  36933  fscgr  36937  idinside  36941  btwnconn1lem11  36954  btwnconn1lem12  36955  btwnconn3  36960  brsegle  36965  seglecgr12  36968  hilbert1.2  37012  exp5d  37183  exp5k  37185  nn0prpwlem  37202  mh-inf3f1  37421  bj-restb  38107  exrecfnlem  38395  poimirlem26  38657  poimirlem29  38660  poimirlem32  38663  areacirc  38724  heibor1lem  38836  pridl  39064  pridlc  39098  dmnnzd  39102  disjlem17  39927  membpartlem19  39939  prtlem11  40016  prtlem17  40026  ax12indn  40093  atcvrj0  40578  cvrat4  40593  athgt  40606  lplnexllnN  40714  2llnjN  40717  lvolnle3at  40732  lncmp  40933  paddclN  40992  pexmidlem4N  41123  cdleme17d3  41646  cdleme50trn2  41701  cdlemf2  41712  cdlemf  41713  cdlemj3  41973  cdlemk26b-3  42055  dihord5b  42409  isnacs3  43814  jm2.26  44102  ordnexbtwnsuc  44362  omabs2  44427  naddgeoa  44489  sbiota1  45511  exbir  45555  tratrb  45612  onfrALT  45625  in2an  45684  pwtrrVD  45900  suctrALT2VD  45911  suctrALT2  45912  tratrbVD  45936  trintALTVD  45955  trintALT  45956  cocanss2  46015  or2expropbi  48197  fcoresf1  48232  2reu8i  48276  2reuimp  48278  zm1nn  48465  2ffzoeq  48491  iccpartiltu  48597  iccpartigtl  48598  iccpartgt  48602  iccpartnel  48613  sbcpr  48696  fmtnofac2lem  48746  fmtnofac2  48747  lighneallem2  48784  odd2prm2  48909  stgoldbwt  48967  sbgoldbst  48969  sbgoldbaltlem1  48970  mogoldbb  48976  uhgrimisgrgric  49122  clnbgrgrim  49125  grimedg  49126  gpgedgvtx1  49253  gpgedg2iv  49258  pgnbgreunbgrlem3  49309  pgnbgreunbgrlem6  49315  pgnbgreunbgr  49316  lidldomn1  49421  idomnzd  49536  ply1mulgsumlem1  49591  lincsumcl  49636  ellcoellss  49640  islinindfis  49654  lindslinindsimp1  49662  lindslinindsimp2lem5  49667  lindsrng01  49673  elfzolborelfzop1  49724  rrx2linest  49947  aacllem  51107