MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expd Structured version   Visualization version   GIF version

Theorem expd 402
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
StepHypRef Expression
1 expd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expdcom 401 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
32com3r 87 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  expcomd  404  expdcomOLD  405  exp32  409  exp4b  419  exp4c  421  exp4d  422  exp42  424  exp44  426  exp5c  433  exp5j  434  exp5l  435  pm3.3  437  expdimp  442  impl  445  syland  592  mpan2d  677  a2and  862  3impib  1137  exp5o  1457  ralrimivv  3169  mob2  3595  reuind  3620  reupick3  4124  elpwunsn  4428  disjiun  4843  sotr2  5274  wefrc  5318  relop  5487  predpoirr  5934  predfrirr  5935  fnun  6217  mpteqb  6529  tpres  6700  fconst5  6705  funfvima  6726  riotaeqimp  6867  dfwe2  7220  limuni3  7291  tfisi  7297  ordom  7313  funcnvuni  7358  f1oweALT  7391  frxp  7530  poxp  7532  wfr3g  7657  wfrlem12  7671  onfununi  7683  tz7.48lem  7781  oecl  7863  oaordex  7884  oaass  7887  omwordri  7898  odi  7905  omass  7906  omeu  7911  oen0  7912  oewordi  7917  oewordri  7918  nnarcl  7942  nnmass  7950  dif1en  8441  findcard2  8448  unblem1  8460  unblem2  8461  domunfican  8481  marypha1lem  8587  supiso  8629  inf3lem3  8783  epfrs  8863  karden  9014  infxpenlem  9128  iunfictbso  9229  dfac5  9243  dfac2b  9245  dfac2OLD  9247  kmlem1  9266  kmlem9  9274  infpssrlem3  9421  fin23lem25  9440  fin23lem30  9458  domtriomlem  9558  axdc3lem4  9569  axcclem  9573  zorn2lem7  9618  konigthlem  9684  wunr1om  9835  tskr1om  9883  gruen  9928  grur1a  9935  indpi  10023  genpnmax  10123  prlem934  10149  ltaddpr  10150  ltexprlem7  10158  ltaprlem  10160  axrrecex  10278  axpre-sup  10284  lelttr  10422  dedekind  10494  addid2  10513  nn0lt2  11725  fzind  11760  fnn0ind  11761  btwnz  11764  uzwo  11989  lbzbi  12014  rpnnen1lem5  12056  ledivge1le  12134  xrlelttr  12224  qbtwnre  12267  xrsupsslem  12374  xrinfmsslem  12375  supxrun  12383  elfz1b  12651  elfz0ubfz0  12686  elfzo0z  12753  fzofzim  12758  elfznelfzo  12816  fleqceilz  12896  fsequb  13017  leexp2r  13160  bernneq  13232  fi1uzind  13515  brfi1indALT  13518  swrdnd2  13676  swrdswrdlem  13702  swrdswrd  13703  wrd2ind  13720  swrdccatin1  13726  swrdccatin2  13730  swrdccatin12lem3  13733  repswswrd  13774  cshweqrep  13810  swrd2lsw  13939  2swrd2eqwrdeq  13940  wrdl3s3  13949  s3iunsndisj  13951  cau3lem  14336  climuni  14525  mulcn2  14568  dvdsabseq  15277  divalglem8  15362  ndvdssub  15371  rplpwr  15514  algcvgblem  15528  lcmf  15584  lcmftp  15587  lcmfunsnlem2lem1  15589  lcmfunsnlem2lem2  15590  lcmfdvdsb  15594  lcmfun  15596  euclemma  15661  prmlem1a  16044  setsstruct2  16126  iscatd  16557  initoeu1  16884  initoeu2  16889  termoeu1  16891  plelttr  17196  grpinveu  17680  symgfixelsi  18075  efgred  18381  telgsumfzs  18607  srgmulgass  18752  srgbinom  18766  lspdisjb  19352  mplcoe5lem  19695  cply1mul  19891  coe1fzgsumd  19899  gsummoncoe1  19901  evl1gsumd  19948  cpmatacl  20754  cpmatmcllem  20756  basis2  20989  0ntr  21109  uncmp  21440  1stcrest  21490  txcls  21641  txcnp  21657  tx1stc  21687  fgss2  21911  alexsubALTlem2  22085  alexsubALTlem3  22086  alexsubALTlem4  22087  metcnp3  22578  tngngp3  22693  reconn  22864  iscau4  23310  ellimc3  23879  ulmbdd  24388  ulmcn  24389  sinq12ge0  24497  logblog  24766  gausslemma2dlem3  25329  ax5seglem5  26049  ax5seg  26054  uhgrnbgr0nb  26488  cplgrop  26583  wlkl1loop  26784  uspgr2wlkeq  26792  wlkres  26817  upgrwlkdvdelem  26882  uhgrwkspthlem2  26900  pthdlem2lem  26913  uspgrn2crct  26951  wlkiswwlks2lem3  27020  wlkiswwlks2  27024  wlkiswwlksupgr2  27026  wlklnwwlkln2lem  27031  wwlksnext  27052  wwlksnextfun  27057  rusgrnumwwlk  27139  clwlkclwwlklem2a4  27162  clwlkclwwlklem3  27166  erclwwlksym  27186  erclwwlknsym  27243  eleclclwwlkn  27249  clwwlknonwwlknonb  27296  upgr3v3e3cycl  27375  upgr4cycl4dv4e  27380  conngrv2edg  27390  eupth2lem3lem6  27428  frgrncvvdeqlem8  27503  frgrwopreglem4a  27507  frgrreggt1  27603  frgrreg  27604  grpoinveu  27724  ococss  28502  shmodsi  28598  h1datomi  28790  hoaddsub  29025  adjmul  29301  chjatom  29566  atomli  29591  atcvat4i  29606  mdsymlem3  29614  mdsymlem5  29616  mdsymlem6  29617  sumdmdlem  29627  cdj3lem2a  29645  cdj3lem3a  29648  bnj1204  31424  cvmsdisj  31596  fundmpss  32007  dfon2lem6  32034  dfon2lem8  32036  frr3g  32121  ifscgr  32493  lineext  32525  fscgr  32529  idinside  32533  btwnconn1lem11  32546  btwnconn1lem12  32547  btwnconn3  32552  brsegle  32557  seglecgr12  32560  hilbert1.2  32604  exp5d  32638  exp5k  32640  nn0prpwlem  32659  bj-restb  33376  poimirlem26  33766  poimirlem29  33769  poimirlem32  33772  areacirc  33835  heibor1lem  33937  pridl  34165  pridlc  34199  dmnnzd  34203  prtlem11  34663  prtlem17  34673  ax12indn  34740  atcvrj0  35226  cvrat4  35241  athgt  35254  lplnexllnN  35362  2llnjN  35365  lvolnle3at  35380  lncmp  35581  paddclN  35640  pexmidlem4N  35771  cdleme17d3  36294  cdleme50trn2  36349  cdlemf2  36360  cdlemf  36361  cdlemj3  36621  cdlemk26b-3  36703  dihord5b  37057  isnacs3  37792  jm2.26  38087  sbiota1  39151  exbir  39199  tratrb  39261  onfrALT  39279  in2an  39348  pwtrrVD  39571  suctrALT2VD  39582  suctrALT2  39583  tratrbVD  39608  trintALTVD  39627  trintALT  39628  zm1nn  41909  2ffzoeq  41930  iccpartiltu  41950  iccpartigtl  41951  iccpartgt  41955  iccpartnel  41966  fmtnofac2lem  42072  fmtnofac2  42073  lighneallem2  42115  odd2prm2  42219  stgoldbwt  42256  sbgoldbst  42258  sbgoldbaltlem1  42259  mogoldbb  42265  lidldomn1  42506  ply1mulgsumlem1  42759  lincsumcl  42805  ellcoellss  42809  islinindfis  42823  lindslinindsimp1  42831  lindslinindsimp2lem5  42836  lindsrng01  42842  elfzolborelfzop1  42894  aacllem  43135
  Copyright terms: Public domain W3C validator