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  3209  mob2  3681  reuind  3719  reupick3  4286  elpwunsn  4655  disjiun  5102  sotr2  5608  wefrc  5660  relop  5841  predpoirr  6341  predfrirr  6342  fnun  6656  mpteqb  7016  tpres  7206  fconst5  7211  funfvima  7235  riotaeqimp  7406  dfwe2  7782  limuni3  7857  tfisi  7864  trom  7880  funcnvuni  7938  resf1ext2b  7941  f1oweALT  7978  frxp  8131  poxp  8133  poxp2  8148  poxp3  8155  wfr3g  8325  onfununi  8337  tz7.48lem  8437  oecl  8531  oaordex  8552  oaass  8555  omwordri  8566  odi  8573  omass  8574  omeu  8579  oen0  8581  oewordi  8586  oewordri  8587  nnarcl  8611  nnmass  8619  brinxper  8733  findcard2  9159  rex2dom  9223  dif1ennnALT  9247  unblem1  9262  unblem2  9263  domunfican  9291  marypha1lem  9403  supiso  9446  inf3lem3  9609  epfrs  9710  frr3g  9738  kardenOLD  9899  infxpenlem  10016  iunfictbso  10117  dfac5  10131  dfac2b  10133  kmlem1  10153  kmlem9  10161  infpssrlem3  10307  fin23lem25  10326  fin23lem30  10344  domtriomlem  10444  axdc3lem4  10455  axcclem  10459  zorn2lem7  10504  konigthlem  10571  wunr1om  10722  tskr1om  10770  gruen  10815  grur1a  10822  indpi  10910  genpnmax  11010  prlem934  11036  ltaddpr  11037  ltexprlem7  11045  ltaprlem  11047  axrrecex  11166  axpre-sup  11172  lelttr  11318  dedekind  11391  addlid  11411  nn0lt2  12677  fzind  12712  fnn0ind  12713  btwnz  12717  uzwo  12953  lbzbi  12978  rpnnen1lem5  13023  ledivge1le  13107  xrlelttr  13199  qbtwnre  13243  xrsupsslem  13351  xrinfmsslem  13352  supxrun  13360  elfz1b  13640  elfz0ubfz0  13679  elfzo0z  13749  fzofzim  13757  elfznelfzo  13821  fleqceilz  13907  fsequb  14031  leexp2r  14230  bernneq  14285  fi1uzind  14564  brfi1indALT  14567  swrdnd0  14719  swrdswrdlem  14765  swrdswrd  14766  wrd2ind  14784  swrdccatin1  14786  swrdccatin2  14790  pfxccatin12lem3  14793  repswswrd  14847  cshweqrep  14884  swrd2lsw  15015  2swrd2eqwrdeq  15016  wrdl3s3  15025  s3iunsndisj  15031  cau3lem  15432  climuni  15629  mulcn2  15673  dvdsabseq  16396  divalglem8  16483  ndvdssub  16492  rplpwr  16641  algcvgblem  16660  lcmf  16716  lcmftp  16719  lcmfunsnlem2lem1  16721  lcmfunsnlem2lem2  16722  lcmfdvdsb  16726  lcmfun  16728  euclemma  16797  prmlem1a  17191  setsstruct2  17259  iscatd  17754  initoeu1  18093  initoeu2  18098  termoeu1  18100  plelttr  18423  insubm  18908  grpinveu  19072  cyccom  19305  symgfixelsi  19536  efgred  19849  telgsumfzs  20090  srgmulgass  20330  srgbinom  20344  lspdisjb  21287  mplcoe5lem  22227  cply1mul  22493  coe1fzgsumd  22501  gsummoncoe1  22505  evl1gsumd  22554  cpmatacl  22910  cpmatmcllem  22912  basis2  23145  0ntr  23265  uncmp  23597  1stcrest  23647  txcls  23798  txcnp  23814  tx1stc  23844  fgss2  24068  alexsubALTlem2  24242  alexsubALTlem3  24243  alexsubALTlem4  24244  metcnp3  24734  tngngp3  24850  reconn  25023  iscau4  25475  ellimc3  26075  ulmbdd  26598  ulmcn  26599  sinq12ge0  26710  gausslemma2dlem3  27569  2sq2  27634  2sqreultlem  27648  2sqreunnltlem  27651  sltsleft  28090  sltsright  28091  noseqind  28522  oldfib  28607  expsgt0  28667  bdayfinbndlem1  28697  bdayfin  28717  elreno2  28725  ax5seglem5  29320  ax5seg  29325  uhgrnbgr0nb  29741  cplgrop  29824  wlkl1loop  30024  uspgr2wlkeq  30032  upgrwlkdvdelem  30122  uhgrwkspthlem2  30140  pthdlem2lem  30153  uspgrn2crct  30194  wlkiswwlks2lem3  30257  wlkiswwlks2  30261  wlkiswwlksupgr2  30263  wlklnwwlkln2lem  30268  wwlksnext  30279  wwlksnextfun  30284  rusgrnumwwlk  30364  clwlkclwwlklem2a4  30385  clwlkclwwlklem3  30389  erclwwlksym  30409  erclwwlknsym  30458  eleclclwwlkn  30464  clwwlknonwwlknonb  30494  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  conngrv2edg  30583  eupth2lem3lem6  30621  frgrncvvdeqlem8  30694  frgrwopreglem4a  30698  frgrreggt1  30781  frgrreg  30782  grpoinveu  30908  ococss  31682  shmodsi  31778  h1datomi  31970  hoaddsub  32205  adjmul  32481  chjatom  32746  atomli  32771  atcvat4i  32786  mdsymlem3  32794  mdsymlem5  32796  mdsymlem6  32797  sumdmdlem  32807  cdj3lem2a  32825  cdj3lem3a  32828  bnj1204  35432  fineqvinfep  35562  umgr2cycllem  35653  umgr2cycl  35654  cvmsdisj  35783  satfv0fun  35884  satffunlem  35914  satffunlem1lem2  35916  satffunlem2lem2  35919  fundmpss  36280  dfon2lem6  36299  dfon2lem8  36301  ifscgr  36557  lineext  36589  fscgr  36593  idinside  36597  btwnconn1lem11  36610  btwnconn1lem12  36611  btwnconn3  36616  brsegle  36621  seglecgr12  36624  hilbert1.2  36668  exp5d  36855  exp5k  36857  nn0prpwlem  36874  mh-inf3f1  37093  bj-restb  37777  exrecfnlem  38066  poimirlem26  38338  poimirlem29  38341  poimirlem32  38344  areacirc  38405  heibor1lem  38501  pridl  38729  pridlc  38763  dmnnzd  38767  disjlem17  39592  membpartlem19  39604  prtlem11  39681  prtlem17  39691  ax12indn  39758  atcvrj0  40243  cvrat4  40258  athgt  40271  lplnexllnN  40379  2llnjN  40382  lvolnle3at  40397  lncmp  40598  paddclN  40657  pexmidlem4N  40788  cdleme17d3  41311  cdleme50trn2  41366  cdlemf2  41377  cdlemf  41378  cdlemj3  41638  cdlemk26b-3  41720  dihord5b  42074  isnacs3  43482  jm2.26  43770  ordnexbtwnsuc  44035  omabs2  44100  naddgeoa  44162  sbiota1  45185  exbir  45229  tratrb  45286  onfrALT  45299  in2an  45358  pwtrrVD  45574  suctrALT2VD  45585  suctrALT2  45586  tratrbVD  45610  trintALTVD  45629  trintALT  45630  or2expropbi  47812  fcoresf1  47847  2reu8i  47891  2reuimp  47893  zm1nn  48080  2ffzoeq  48106  iccpartiltu  48212  iccpartigtl  48213  iccpartgt  48217  iccpartnel  48228  sbcpr  48311  fmtnofac2lem  48361  fmtnofac2  48362  lighneallem2  48399  odd2prm2  48524  stgoldbwt  48582  sbgoldbst  48584  sbgoldbaltlem1  48585  mogoldbb  48591  uhgrimisgrgric  48737  clnbgrgrim  48740  grimedg  48741  gpgedgvtx1  48868  gpgedg2iv  48873  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem6  48930  pgnbgreunbgr  48931  lidldomn1  49037  idomnzd  49152  ply1mulgsumlem1  49207  lincsumcl  49252  ellcoellss  49256  islinindfis  49270  lindslinindsimp1  49278  lindslinindsimp2lem5  49283  lindsrng01  49289  elfzolborelfzop1  49340  rrx2linest  49563  aacllem  50662