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

Theorem expd 452
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 450 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
43com3r 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 197  df-an 386
This theorem is referenced by:  expdimp  453  expcomd  454  expdcom  455  pm3.3  460  syland  498  exp32  630  exp4b  631  exp4c  635  exp4d  636  exp42  638  exp44  640  exp5c  643  exp5j  644  exp5l  645  impl  649  mpan2d  709  a2and  852  3impib  1259  exp5o  1283  ax7  1940  ralrimivv  2966  mob2  3373  reuind  3398  reupick3  3894  elpwunsn  4202  disjiun  4613  sotr2  5034  wefrc  5078  relop  5242  predpoirr  5677  predfrirr  5678  suctrOLD  5778  fnun  5965  mpteqb  6265  funopsn  6378  tpres  6431  fconst5  6436  funfvima  6457  riotaeqimp  6599  dfwe2  6943  limuni3  7014  tfisi  7020  ordom  7036  funcnvuni  7081  f1oweALT  7112  frxp  7247  poxp  7249  wfr3g  7373  wfrlem12  7386  onfununi  7398  tz7.48lem  7496  oecl  7577  oaordex  7598  oaass  7601  omwordri  7612  odi  7619  omass  7620  omeu  7625  oen0  7626  oewordi  7631  oewordri  7632  nnarcl  7656  nnmass  7664  dif1en  8153  findcard2  8160  unblem1  8172  unblem2  8173  domunfican  8193  marypha1lem  8299  supiso  8341  inf3lem3  8487  epfrs  8567  karden  8718  infxpenlem  8796  iunfictbso  8897  dfac5  8911  dfac2  8913  kmlem1  8932  kmlem9  8940  infpssrlem3  9087  fin23lem25  9106  fin23lem30  9124  domtriomlem  9224  axdc3lem4  9235  axcclem  9239  zorn2lem7  9284  konigthlem  9350  wunr1om  9501  tskr1om  9549  gruen  9594  grur1a  9601  indpi  9689  genpnmax  9789  prlem934  9815  ltaddpr  9816  ltexprlem7  9824  ltaprlem  9826  axrrecex  9944  axpre-sup  9950  lelttr  10088  dedekind  10160  addid2  10179  nn0lt2  11400  fzind  11435  fnn0ind  11436  btwnz  11439  uzwo  11711  lbzbi  11736  rpnnen1lem5  11778  rpnnen1lem5OLD  11784  ledivge1le  11861  xrlelttr  11947  qbtwnre  11989  xrsupsslem  12096  xrinfmsslem  12097  supxrun  12105  elfz0ubfz0  12400  elfzo0z  12466  fzofzim  12471  elfznelfzo  12530  fleqceilz  12609  fsequb  12730  leexp2r  12874  bernneq  12946  fi1uzind  13234  brfi1indALT  13237  fi1uzindOLD  13240  brfi1indALTOLD  13243  swrdnd2  13387  swrdswrdlem  13413  swrdswrd  13414  wrd2ind  13431  swrdccatin1  13436  swrdccatin2  13440  swrdccatin12lem3  13443  repswswrd  13484  cshweqrep  13520  swrd2lsw  13645  2swrd2eqwrdeq  13646  wrdl3s3  13655  s3iunsndisj  13657  cau3lem  14044  climuni  14233  mulcn2  14276  dvdsabseq  14978  divalglem8  15066  ndvdssub  15076  rplpwr  15219  algcvgblem  15233  lcmf  15289  lcmftp  15292  lcmfunsnlem2lem1  15294  lcmfunsnlem2lem2  15295  lcmfdvdsb  15299  lcmfun  15301  cncongr1  15324  euclemma  15368  prmlem1a  15756  setsstruct2  15836  iscatd  16274  initoeu1  16601  initoeu2  16606  termoeu1  16608  plelttr  16912  grpinveu  17396  symgfixelsi  17795  efgred  18101  telgsumfzs  18326  srgmulgass  18471  srgbinom  18485  lspdisjb  19066  mplcoe5lem  19407  cply1mul  19604  coe1fzgsumd  19612  gsummoncoe1  19614  evl1gsumd  19661  cpmatacl  20461  cpmatmcllem  20463  basis2  20695  0ntr  20815  uncmp  21146  1stcrest  21196  txcls  21347  txcnp  21363  tx1stc  21393  fgss2  21618  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  metcnp3  22285  tngngp3  22400  reconn  22571  iscau4  23017  ellimc3  23583  ulmbdd  24090  ulmcn  24091  sinq12ge0  24198  logblog  24464  gausslemma2dlem3  25027  ax5seglem5  25747  ax5seg  25752  uhgrnbgr0nb  26171  cplgrop  26254  wlkl1loop  26437  uspgr2wlkeq  26445  wlkres  26470  upgrwlkdvdelem  26535  uhgrwkspthlem2  26553  pthdlem2lem  26566  uspgrn2crct  26603  wlkiswwlks2lem3  26660  wlkiswwlks2  26664  wlkiswwlksupgr2  26666  wlklnwwlkln2lem  26671  wwlksnext  26691  wwlksnextfun  26696  rusgrnumwwlk  26771  clwlkclwwlklem2a4  26799  clwlkclwwlklem3  26803  erclwwlkssym  26835  erclwwlksnsym  26847  eleclclwwlksn  26853  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  conngrv2edg  26955  eupth2lem3lem6  26993  frgrncvvdeqlemB  27069  frgrwopreglem5  27077  numclwwlkovf2ex  27109  numclwlk1lem2f1  27116  frgrreggt1  27139  frgrreg  27140  grpoinveu  27261  ococss  28040  shmodsi  28136  h1datomi  28328  hoaddsub  28563  adjmul  28839  chjatom  29104  atomli  29129  atcvat4i  29144  mdsymlem3  29152  mdsymlem5  29154  mdsymlem6  29155  sumdmdlem  29165  cdj3lem2a  29183  cdj3lem3a  29186  bnj1204  30841  cvmsdisj  31013  fundmpss  31421  dfon2lem6  31447  dfon2lem8  31449  frr3g  31533  frrlem11  31546  slttr3  31589  noprefixmo  31626  ifscgr  31846  lineext  31878  fscgr  31882  idinside  31886  btwnconn1lem11  31899  btwnconn1lem12  31900  btwnconn3  31905  brsegle  31910  seglecgr12  31913  hilbert1.2  31957  exp5d  31991  exp5k  31993  nn0prpwlem  32012  bj-restb  32737  poimirlem26  33106  poimirlem29  33109  poimirlem32  33112  areacirc  33176  heibor1lem  33279  pridl  33507  pridlc  33541  dmnnzd  33545  prtlem11  33670  prtlem17  33680  ax12indn  33747  atcvrj0  34233  cvrat4  34248  athgt  34261  lplnexllnN  34369  2llnjN  34372  lvolnle3at  34387  lncmp  34588  paddclN  34647  pexmidlem4N  34778  cdleme17d3  35303  cdleme50trn2  35358  cdlemf2  35369  cdlemf  35370  cdlemj3  35630  cdlemk26b-3  35712  dihord5b  36067  isnacs3  36792  jm2.26  37088  sbiota1  38156  exbir  38205  tratrb  38267  onfrALT  38285  in2an  38354  pwtrrVD  38582  suctrALT2VD  38593  suctrALT2  38594  tratrbVD  38619  trintALTVD  38638  trintALT  38639  zm1nn  40643  2ffzoeq  40665  iccpartiltu  40686  iccpartigtl  40687  iccpartgt  40691  iccpartnel  40702  fmtnofac2lem  40809  fmtnofac2  40810  lighneallem2  40852  stgoldbwt  40989  bgoldbst  40991  sgoldbaltlem1  40992  lidldomn1  41239  ply1mulgsumlem1  41492  lincsumcl  41538  ellcoellss  41542  islinindfis  41556  lindslinindsimp1  41564  lindslinindsimp2lem5  41569  lindsrng01  41575  elfzolborelfzop1  41627  aacllem  41880
  Copyright terms: Public domain W3C validator