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

Theorem expd 451
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
expd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
expd (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem expd
StepHypRef Expression
1 expd.1 . . . 4 (𝜑 → ((𝜓𝜒) → 𝜃))
21com12 32 . . 3 ((𝜓𝜒) → (𝜑𝜃))
32ex 449 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
43com3r 87 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  expdimp  452  expcomd  453  expdcom  454  pm3.3  459  syland  499  exp32  632  exp4b  633  exp4c  637  exp4d  638  exp42  640  exp44  642  exp5c  645  exp5j  646  exp5l  647  impl  651  mpan2d  712  a2and  888  3impib  1109  exp5o  1449  ax7  2098  ralrimivv  3108  mob2  3527  reuind  3552  reupick3  4055  elpwunsn  4368  disjiun  4792  sotr2  5216  wefrc  5260  relop  5428  predpoirr  5869  predfrirr  5870  suctrOLD  5970  fnun  6158  mpteqb  6461  funopsn  6576  tpres  6630  fconst5  6635  funfvima  6655  riotaeqimp  6797  dfwe2  7146  limuni3  7217  tfisi  7223  ordom  7239  funcnvuni  7284  f1oweALT  7317  frxp  7455  poxp  7457  wfr3g  7582  wfrlem12  7595  onfununi  7607  tz7.48lem  7705  oecl  7786  oaordex  7807  oaass  7810  omwordri  7821  odi  7828  omass  7829  omeu  7834  oen0  7835  oewordi  7840  oewordri  7841  nnarcl  7865  nnmass  7873  dif1en  8358  findcard2  8365  unblem1  8377  unblem2  8378  domunfican  8398  marypha1lem  8504  supiso  8546  inf3lem3  8700  epfrs  8780  karden  8931  infxpenlem  9026  iunfictbso  9127  dfac5  9141  dfac2b  9143  dfac2OLD  9145  kmlem1  9164  kmlem9  9172  infpssrlem3  9319  fin23lem25  9338  fin23lem30  9356  domtriomlem  9456  axdc3lem4  9467  axcclem  9471  zorn2lem7  9516  konigthlem  9582  wunr1om  9733  tskr1om  9781  gruen  9826  grur1a  9833  indpi  9921  genpnmax  10021  prlem934  10047  ltaddpr  10048  ltexprlem7  10056  ltaprlem  10058  axrrecex  10176  axpre-sup  10182  lelttr  10320  dedekind  10392  addid2  10411  nn0lt2  11632  fzind  11667  fnn0ind  11668  btwnz  11671  uzwo  11944  lbzbi  11969  rpnnen1lem5  12011  rpnnen1lem5OLD  12017  ledivge1le  12094  xrlelttr  12180  qbtwnre  12223  xrsupsslem  12330  xrinfmsslem  12331  supxrun  12339  elfz1b  12602  elfz0ubfz0  12637  elfzo0z  12704  fzofzim  12709  elfznelfzo  12767  fleqceilz  12847  fsequb  12968  leexp2r  13112  bernneq  13184  fi1uzind  13471  brfi1indALT  13474  swrdnd2  13633  swrdswrdlem  13659  swrdswrd  13660  wrd2ind  13677  swrdccatin1  13683  swrdccatin2  13687  swrdccatin12lem3  13690  repswswrd  13731  cshweqrep  13767  swrd2lsw  13896  2swrd2eqwrdeq  13897  wrdl3s3  13906  s3iunsndisj  13908  cau3lem  14293  climuni  14482  mulcn2  14525  dvdsabseq  15237  divalglem8  15325  ndvdssub  15335  rplpwr  15478  algcvgblem  15492  lcmf  15548  lcmftp  15551  lcmfunsnlem2lem1  15553  lcmfunsnlem2lem2  15554  lcmfdvdsb  15558  lcmfun  15560  euclemma  15627  prmlem1a  16015  setsstruct2  16098  iscatd  16535  initoeu1  16862  initoeu2  16867  termoeu1  16869  plelttr  17173  grpinveu  17657  symgfixelsi  18055  efgred  18361  telgsumfzs  18586  srgmulgass  18731  srgbinom  18745  lspdisjb  19328  mplcoe5lem  19669  cply1mul  19866  coe1fzgsumd  19874  gsummoncoe1  19876  evl1gsumd  19923  cpmatacl  20723  cpmatmcllem  20725  basis2  20957  0ntr  21077  uncmp  21408  1stcrest  21458  txcls  21609  txcnp  21625  tx1stc  21655  fgss2  21879  alexsubALTlem2  22053  alexsubALTlem3  22054  alexsubALTlem4  22055  metcnp3  22546  tngngp3  22661  reconn  22832  iscau4  23277  ellimc3  23842  ulmbdd  24351  ulmcn  24352  sinq12ge0  24459  logblog  24729  gausslemma2dlem3  25292  ax5seglem5  26012  ax5seg  26017  uhgrnbgr0nb  26449  cplgrop  26543  wlkl1loop  26744  uspgr2wlkeq  26752  wlkres  26777  upgrwlkdvdelem  26842  uhgrwkspthlem2  26860  pthdlem2lem  26873  uspgrn2crct  26911  wlkiswwlks2lem3  26980  wlkiswwlks2  26984  wlkiswwlksupgr2  26986  wlklnwwlkln2lem  26991  wwlksnext  27011  wwlksnextfun  27016  rusgrnumwwlk  27097  clwlkclwwlklem2a4  27120  clwlkclwwlklem3  27124  erclwwlksym  27144  erclwwlknsym  27201  eleclclwwlkn  27207  clwwlknonwwlknonb  27254  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  conngrv2edg  27347  eupth2lem3lem6  27385  frgrncvvdeqlem8  27460  frgrwopreglem4a  27464  frgrreggt1  27561  frgrreg  27562  grpoinveu  27682  ococss  28461  shmodsi  28557  h1datomi  28749  hoaddsub  28984  adjmul  29260  chjatom  29525  atomli  29550  atcvat4i  29565  mdsymlem3  29573  mdsymlem5  29575  mdsymlem6  29576  sumdmdlem  29586  cdj3lem2a  29604  cdj3lem3a  29607  bnj1204  31387  cvmsdisj  31559  fundmpss  31971  dfon2lem6  31998  dfon2lem8  32000  frr3g  32085  ifscgr  32457  lineext  32489  fscgr  32493  idinside  32497  btwnconn1lem11  32510  btwnconn1lem12  32511  btwnconn3  32516  brsegle  32521  seglecgr12  32524  hilbert1.2  32568  exp5d  32602  exp5k  32604  nn0prpwlem  32623  bj-restb  33353  poimirlem26  33748  poimirlem29  33751  poimirlem32  33754  areacirc  33818  heibor1lem  33921  pridl  34149  pridlc  34183  dmnnzd  34187  prtlem11  34655  prtlem17  34665  ax12indn  34732  atcvrj0  35217  cvrat4  35232  athgt  35245  lplnexllnN  35353  2llnjN  35356  lvolnle3at  35371  lncmp  35572  paddclN  35631  pexmidlem4N  35762  cdleme17d3  36286  cdleme50trn2  36341  cdlemf2  36352  cdlemf  36353  cdlemj3  36613  cdlemk26b-3  36695  dihord5b  37050  isnacs3  37775  jm2.26  38071  sbiota1  39137  exbir  39186  tratrb  39248  onfrALT  39266  in2an  39335  pwtrrVD  39559  suctrALT2VD  39570  suctrALT2  39571  tratrbVD  39596  trintALTVD  39615  trintALT  39616  zm1nn  41826  2ffzoeq  41848  iccpartiltu  41868  iccpartigtl  41869  iccpartgt  41873  iccpartnel  41884  fmtnofac2lem  41990  fmtnofac2  41991  lighneallem2  42033  odd2prm2  42137  stgoldbwt  42174  sbgoldbst  42176  sbgoldbaltlem1  42177  mogoldbb  42183  lidldomn1  42431  ply1mulgsumlem1  42684  lincsumcl  42730  ellcoellss  42734  islinindfis  42748  lindslinindsimp1  42756  lindslinindsimp2lem5  42761  lindsrng01  42767  elfzolborelfzop1  42819  aacllem  43060
  Copyright terms: Public domain W3C validator