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  497  exp32  630  exp4b  631  exp4c  635  exp4d  636  exp42  638  exp44  640  exp5c  643  exp5j  644  exp5l  645  impl  649  mpan2d  710  a2and  870  3impib  1281  exp5o  1308  ax7  1989  ralrimivv  2999  mob2  3419  reuind  3444  reupick3  3945  elpwunsn  4256  disjiun  4672  sotr2  5093  wefrc  5137  relop  5305  predpoirr  5746  predfrirr  5747  suctrOLD  5847  fnun  6035  mpteqb  6338  funopsn  6453  tpres  6507  fconst5  6512  funfvima  6532  riotaeqimp  6674  dfwe2  7023  limuni3  7094  tfisi  7100  ordom  7116  funcnvuni  7161  f1oweALT  7194  frxp  7332  poxp  7334  wfr3g  7458  wfrlem12  7471  onfununi  7483  tz7.48lem  7581  oecl  7662  oaordex  7683  oaass  7686  omwordri  7697  odi  7704  omass  7705  omeu  7710  oen0  7711  oewordi  7716  oewordri  7717  nnarcl  7741  nnmass  7749  dif1en  8234  findcard2  8241  unblem1  8253  unblem2  8254  domunfican  8274  marypha1lem  8380  supiso  8422  inf3lem3  8565  epfrs  8645  karden  8796  infxpenlem  8874  iunfictbso  8975  dfac5  8989  dfac2  8991  kmlem1  9010  kmlem9  9018  infpssrlem3  9165  fin23lem25  9184  fin23lem30  9202  domtriomlem  9302  axdc3lem4  9313  axcclem  9317  zorn2lem7  9362  konigthlem  9428  wunr1om  9579  tskr1om  9627  gruen  9672  grur1a  9679  indpi  9767  genpnmax  9867  prlem934  9893  ltaddpr  9894  ltexprlem7  9902  ltaprlem  9904  axrrecex  10022  axpre-sup  10028  lelttr  10166  dedekind  10238  addid2  10257  nn0lt2  11478  fzind  11513  fnn0ind  11514  btwnz  11517  uzwo  11789  lbzbi  11814  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  ledivge1le  11939  xrlelttr  12025  qbtwnre  12068  xrsupsslem  12175  xrinfmsslem  12176  supxrun  12184  elfz1b  12447  elfz0ubfz0  12482  elfzo0z  12549  fzofzim  12554  elfznelfzo  12613  fleqceilz  12693  fsequb  12814  leexp2r  12958  bernneq  13030  fi1uzind  13317  brfi1indALT  13320  swrdnd2  13479  swrdswrdlem  13505  swrdswrd  13506  wrd2ind  13523  swrdccatin1  13529  swrdccatin2  13533  swrdccatin12lem3  13536  repswswrd  13577  cshweqrep  13613  swrd2lsw  13741  2swrd2eqwrdeq  13742  wrdl3s3  13751  s3iunsndisj  13753  cau3lem  14138  climuni  14327  mulcn2  14370  dvdsabseq  15082  divalglem8  15170  ndvdssub  15180  rplpwr  15323  algcvgblem  15337  lcmf  15393  lcmftp  15396  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfdvdsb  15403  lcmfun  15405  euclemma  15472  prmlem1a  15860  setsstruct2  15943  iscatd  16381  initoeu1  16708  initoeu2  16713  termoeu1  16715  plelttr  17019  grpinveu  17503  symgfixelsi  17901  efgred  18207  telgsumfzs  18432  srgmulgass  18577  srgbinom  18591  lspdisjb  19174  mplcoe5lem  19515  cply1mul  19712  coe1fzgsumd  19720  gsummoncoe1  19722  evl1gsumd  19769  cpmatacl  20569  cpmatmcllem  20571  basis2  20803  0ntr  20923  uncmp  21254  1stcrest  21304  txcls  21455  txcnp  21471  tx1stc  21501  fgss2  21725  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  metcnp3  22392  tngngp3  22507  reconn  22678  iscau4  23123  ellimc3  23688  ulmbdd  24197  ulmcn  24198  sinq12ge0  24305  logblog  24575  gausslemma2dlem3  25138  ax5seglem5  25858  ax5seg  25863  uhgrnbgr0nb  26295  cplgrop  26389  wlkl1loop  26590  uspgr2wlkeq  26598  wlkres  26623  upgrwlkdvdelem  26688  uhgrwkspthlem2  26706  pthdlem2lem  26719  uspgrn2crct  26756  wlkiswwlks2lem3  26825  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wwlksnext  26856  wwlksnextfun  26861  rusgrnumwwlk  26942  clwlkclwwlklem2a4  26963  clwlkclwwlklem3  26967  erclwwlksym  26978  erclwwlknsym  27034  eleclclwwlkn  27040  clwwlknonwwlknonb  27080  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  conngrv2edg  27173  eupth2lem3lem6  27211  frgrncvvdeqlem8  27286  frgrwopreglem4a  27290  frgrreggt1  27380  frgrreg  27381  grpoinveu  27501  ococss  28280  shmodsi  28376  h1datomi  28568  hoaddsub  28803  adjmul  29079  chjatom  29344  atomli  29369  atcvat4i  29384  mdsymlem3  29392  mdsymlem5  29394  mdsymlem6  29395  sumdmdlem  29405  cdj3lem2a  29423  cdj3lem3a  29426  bnj1204  31206  cvmsdisj  31378  fundmpss  31790  dfon2lem6  31817  dfon2lem8  31819  frr3g  31904  ifscgr  32276  lineext  32308  fscgr  32312  idinside  32316  btwnconn1lem11  32329  btwnconn1lem12  32330  btwnconn3  32335  brsegle  32340  seglecgr12  32343  hilbert1.2  32387  exp5d  32421  exp5k  32423  nn0prpwlem  32442  bj-restb  33172  poimirlem26  33565  poimirlem29  33568  poimirlem32  33571  areacirc  33635  heibor1lem  33738  pridl  33966  pridlc  34000  dmnnzd  34004  prtlem11  34470  prtlem17  34480  ax12indn  34547  atcvrj0  35032  cvrat4  35047  athgt  35060  lplnexllnN  35168  2llnjN  35171  lvolnle3at  35186  lncmp  35387  paddclN  35446  pexmidlem4N  35577  cdleme17d3  36101  cdleme50trn2  36156  cdlemf2  36167  cdlemf  36168  cdlemj3  36428  cdlemk26b-3  36510  dihord5b  36865  isnacs3  37590  jm2.26  37886  sbiota1  38952  exbir  39001  tratrb  39063  onfrALT  39081  in2an  39150  pwtrrVD  39374  suctrALT2VD  39385  suctrALT2  39386  tratrbVD  39411  trintALTVD  39430  trintALT  39431  zm1nn  41641  2ffzoeq  41663  iccpartiltu  41683  iccpartigtl  41684  iccpartgt  41688  iccpartnel  41699  fmtnofac2lem  41805  fmtnofac2  41806  lighneallem2  41848  odd2prm2  41952  stgoldbwt  41989  sbgoldbst  41991  sbgoldbaltlem1  41992  mogoldbb  41998  lidldomn1  42246  ply1mulgsumlem1  42499  lincsumcl  42545  ellcoellss  42549  islinindfis  42563  lindslinindsimp1  42571  lindslinindsimp2lem5  42576  lindsrng01  42582  elfzolborelfzop1  42634  aacllem  42875
  Copyright terms: Public domain W3C validator