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 85 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 196  df-an 385
This theorem is referenced by:  expdimp  452  expcomd  453  expdcom  454  pm3.3  459  syland  497  exp32  629  exp4b  630  exp4c  634  exp4d  635  exp42  637  exp44  639  exp5c  642  exp5j  643  exp5l  644  impl  648  mpan2d  706  a2and  849  3impib  1254  exp5o  1278  ax7  1930  ralrimivv  2953  mob2  3353  reuind  3378  reupick3  3871  elpwunsn  4171  disjiun  4568  sotr2  4978  wefrc  5022  relop  5182  predpoirr  5611  predfrirr  5612  suctrOLD  5712  fnun  5897  mpteqb  6192  tpres  6349  fconst5  6354  funfvima  6374  dfwe2  6851  limuni3  6922  tfisi  6928  ordom  6944  funcnvuni  6990  f1oweALT  7021  frxp  7152  poxp  7154  wfr3g  7278  wfrlem12  7291  onfununi  7303  tz7.48lem  7401  oecl  7482  oaordex  7503  oaass  7506  omwordri  7517  odi  7524  omass  7525  omeu  7530  oen0  7531  oewordi  7536  oewordri  7537  nnarcl  7561  nnmass  7569  dif1en  8056  findcard2  8063  unblem1  8075  unblem2  8076  domunfican  8096  marypha1lem  8200  supiso  8242  inf3lem3  8388  epfrs  8468  karden  8619  infxpenlem  8697  iunfictbso  8798  dfac5  8812  dfac2  8814  kmlem1  8833  kmlem9  8841  infpssrlem3  8988  fin23lem25  9007  fin23lem30  9025  domtriomlem  9125  axdc3lem4  9136  axcclem  9140  zorn2lem7  9185  konigthlem  9247  wunr1om  9398  tskr1om  9446  gruen  9491  grur1a  9498  indpi  9586  genpnmax  9686  prlem934  9712  ltaddpr  9713  ltexprlem7  9721  ltaprlem  9723  axrrecex  9841  axpre-sup  9847  lelttr  9980  dedekind  10052  addid2  10071  nn0lt2  11276  fzind  11310  fnn0ind  11311  btwnz  11314  uzwo  11586  lbzbi  11611  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  ledivge1le  11736  xrlelttr  11825  qbtwnre  11866  xrsupsslem  11968  xrinfmsslem  11969  supxrun  11977  elfz0ubfz0  12270  elfzo0z  12335  fzofzim  12340  elfznelfzo  12397  fleqceilz  12473  fsequb  12594  leexp2r  12738  bernneq  12810  fi1uzind  13083  brfi1indALT  13086  fi1uzindOLD  13089  brfi1indALTOLD  13092  swrdnd2  13234  swrdswrdlem  13260  swrdswrd  13261  wrd2ind  13278  swrdccatin1  13283  swrdccatin2  13287  swrdccatin12lem3  13290  repswswrd  13331  cshweqrep  13367  swrd2lsw  13492  2swrd2eqwrdeq  13493  wrdl3s3  13502  s3iunsndisj  13504  cau3lem  13891  climuni  14080  mulcn2  14123  dvdsabseq  14822  divalglem8  14910  ndvdssub  14920  rplpwr  15063  algcvgblem  15077  lcmf  15133  lcmftp  15136  lcmfunsnlem2lem1  15138  lcmfunsnlem2lem2  15139  lcmfdvdsb  15143  lcmfun  15145  cncongr1  15168  euclemma  15212  prmlem1a  15600  iscatd  16106  initoeu1  16433  initoeu2  16438  termoeu1  16440  plelttr  16744  grpinveu  17228  symgfixelsi  17627  efgred  17933  telgsumfzs  18158  srgmulgass  18303  srgbinom  18317  lspdisjb  18896  mplcoe5lem  19237  cply1mul  19434  coe1fzgsumd  19442  gsummoncoe1  19444  evl1gsumd  19491  cpmatacl  20288  cpmatmcllem  20290  basis2  20514  0ntr  20633  uncmp  20964  1stcrest  21014  txcls  21165  txcnp  21181  tx1stc  21211  fgss2  21436  alexsubALTlem2  21610  alexsubALTlem3  21611  alexsubALTlem4  21612  metcnp3  22103  tngngp3  22218  reconn  22387  iscau4  22830  ellimc3  23394  ulmbdd  23901  ulmcn  23902  sinq12ge0  24009  logblog  24275  gausslemma2dlem3  24838  ax5seglem5  25559  ax5seg  25564  wlkiswwlk2lem3  26015  wlkiswwlk2  26019  wlklniswwlkn2  26022  usg2wlkeq  26030  wwlknred  26045  wwlknext  26046  wwlkextfun  26051  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem0  26110  wwlksubclwwlk  26126  erclwwlksym  26136  erclwwlknsym  26148  eleclclwwlkn  26154  cusgraisrusgra  26259  rusgranumwlk  26278  eupai  26288  frgrancvvdeqlemB  26359  frgrawopreglem5  26369  frg2woteq  26381  extwwlkfablem2  26399  numclwwlkovf2ex  26407  numclwlk1lem2f1  26415  frgrareggt1  26437  frgrareg  26438  grpoinveu  26551  ococss  27330  shmodsi  27426  h1datomi  27618  hoaddsub  27853  adjmul  28129  chjatom  28394  atomli  28419  atcvat4i  28434  mdsymlem3  28442  mdsymlem5  28444  mdsymlem6  28445  sumdmdlem  28455  cdj3lem2a  28473  cdj3lem3a  28476  bnj1204  30128  cvmsdisj  30300  fundmpss  30704  dfon2lem6  30731  dfon2lem8  30733  frr3g  30817  frrlem11  30830  ifscgr  31115  lineext  31147  fscgr  31151  idinside  31155  btwnconn1lem11  31168  btwnconn1lem12  31169  btwnconn3  31174  brsegle  31179  seglecgr12  31182  hilbert1.2  31226  exp5d  31260  exp5k  31262  nn0prpwlem  31281  bj-restb  32022  poimirlem26  32399  poimirlem29  32402  poimirlem32  32405  areacirc  32469  heibor1lem  32572  pridl  32800  pridlc  32834  dmnnzd  32838  prtlem11  32963  prtlem17  32973  ax12indn  33040  atcvrj0  33526  cvrat4  33541  athgt  33554  lplnexllnN  33662  2llnjN  33665  lvolnle3at  33680  lncmp  33881  paddclN  33940  pexmidlem4N  34071  cdleme17d3  34596  cdleme50trn2  34651  cdlemf2  34662  cdlemf  34663  cdlemj3  34923  cdlemk26b-3  35005  dihord5b  35360  isnacs3  36085  jm2.26  36381  sbiota1  37451  exbir  37499  tratrb  37561  onfrALT  37579  in2an  37648  pwtrrVD  37876  suctrALT2VD  37887  suctrALT2  37888  tratrbVD  37913  trintALTVD  37932  trintALT  37933  iccpartiltu  39755  iccpartigtl  39756  iccpartgt  39760  iccpartnel  39771  fmtnofac2lem  39813  fmtnofac2  39814  lighneallem2  39856  stgoldbwt  39993  bgoldbst  39995  sgoldbaltlem1  39996  funopsn  40134  riotaeqimp  40155  zm1nn  40165  2ffzoeq  40178  uhgrnbgr0nb  40568  cplgrop  40651  1wlkl1loop  40834  uspgr2wlkeq  40846  1wlkres  40871  upgrwlkdvdelem  40934  uhgr1wlkspthlem2  40952  pthdlem2lem  40965  isclWlkb  40972  crctisclwlk  40992  uspgrn2crct  41003  1wlkiswwlks2lem3  41060  1wlkiswwlks2  41064  1wlkiswwlksupgr2  41066  1wlklnwwlkln2lem  41071  wwlksnext  41091  wwlksnextfun  41096  rusgrnumwwlk  41170  clwlkclwwlklem2a4  41198  clwlkclwwlklem3  41202  erclwwlkssym  41234  erclwwlksnsym  41246  eleclclwwlksn  41252  upgr3v3e3cycl  41339  upgr4cycl4dv4e  41344  conngrv2edg  41354  eupth2lem3lem6  41393  frgrncvvdeqlemB  41469  frgrwopreglem5  41477  av-numclwwlkovf2ex  41509  av-numclwlk1lem2f1  41516  av-frgrareggt1  41539  av-frgrareg  41540  lidldomn1  41703  ply1mulgsumlem1  41960  lincsumcl  42006  ellcoellss  42010  islinindfis  42024  lindslinindsimp1  42032  lindslinindsimp2lem5  42037  lindsrng01  42043  elfzolborelfzop1  42095  aacllem  42309
  Copyright terms: Public domain W3C validator