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

Theorem expd 416
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 415 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
32com3r 87 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  expcomd  417  exp32  421  exp4b  431  exp4c  433  exp4d  434  exp42  436  exp44  438  exp5c  445  exp5j  446  exp5l  447  pm3.3  449  expdimp  453  impl  456  syland  602  mpan2d  690  a2and  839  3impib  1108  exp5o  1347  ralrimivv  3187  mob2  3703  reuind  3741  reupick3  4285  elpwunsn  4613  disjiun  5044  sotr2  5498  wefrc  5542  relop  5714  predpoirr  6169  predfrirr  6170  fnun  6456  mpteqb  6779  tpres  6955  fconst5  6960  funfvima  6983  riotaeqimp  7129  dfwe2  7485  limuni3  7556  tfisi  7562  ordom  7578  funcnvuni  7625  f1oweALT  7662  frxp  7809  poxp  7811  wfr3g  7942  wfrlem12  7955  onfununi  7967  tz7.48lem  8066  oecl  8151  oaordex  8173  oaass  8176  omwordri  8187  odi  8194  omass  8195  omeu  8200  oen0  8201  oewordi  8206  oewordri  8207  nnarcl  8231  nnmass  8239  dif1en  8739  findcard2  8746  unblem1  8758  unblem2  8759  domunfican  8779  marypha1lem  8885  supiso  8927  inf3lem3  9081  epfrs  9161  karden  9312  infxpenlem  9427  iunfictbso  9528  dfac5  9542  dfac2b  9544  kmlem1  9564  kmlem9  9572  infpssrlem3  9715  fin23lem25  9734  fin23lem30  9752  domtriomlem  9852  axdc3lem4  9863  axcclem  9867  zorn2lem7  9912  konigthlem  9978  wunr1om  10129  tskr1om  10177  gruen  10222  grur1a  10229  indpi  10317  genpnmax  10417  prlem934  10443  ltaddpr  10444  ltexprlem7  10452  ltaprlem  10454  axrrecex  10573  axpre-sup  10579  lelttr  10719  dedekind  10791  addid2  10811  nn0lt2  12033  fzind  12068  fnn0ind  12069  btwnz  12072  uzwo  12299  lbzbi  12324  rpnnen1lem5  12368  ledivge1le  12448  xrlelttr  12537  qbtwnre  12580  xrsupsslem  12688  xrinfmsslem  12689  supxrun  12697  elfz1b  12964  elfz0ubfz0  12999  elfzo0z  13067  fzofzim  13072  elfznelfzo  13130  fleqceilz  13210  fsequb  13331  leexp2r  13526  bernneq  13578  fi1uzind  13843  brfi1indALT  13846  swrdnd0  14007  swrdswrdlem  14054  swrdswrd  14055  wrd2ind  14073  swrdccatin1  14075  swrdccatin2  14079  pfxccatin12lem3  14082  repswswrd  14134  cshweqrep  14171  swrd2lsw  14302  2swrd2eqwrdeq  14303  wrdl3s3  14314  s3iunsndisj  14316  cau3lem  14702  climuni  14897  mulcn2  14940  dvdsabseq  15651  divalglem8  15739  ndvdssub  15748  rplpwr  15895  algcvgblem  15909  lcmf  15965  lcmftp  15968  lcmfunsnlem2lem1  15970  lcmfunsnlem2lem2  15971  lcmfdvdsb  15975  lcmfun  15977  euclemma  16045  prmlem1a  16428  setsstruct2  16509  iscatd  16932  initoeu1  17259  initoeu2  17264  termoeu1  17266  plelttr  17570  insubm  17971  grpinveu  18076  cyccom  18284  symgfixelsi  18492  efgred  18803  telgsumfzs  19038  srgmulgass  19210  srgbinom  19224  lspdisjb  19827  mplcoe5lem  20176  cply1mul  20390  coe1fzgsumd  20398  gsummoncoe1  20400  evl1gsumd  20448  cpmatacl  21252  cpmatmcllem  21254  basis2  21487  0ntr  21607  uncmp  21939  1stcrest  21989  txcls  22140  txcnp  22156  tx1stc  22186  fgss2  22410  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  metcnp3  23077  tngngp3  23192  reconn  23363  iscau4  23809  ellimc3  24404  ulmbdd  24913  ulmcn  24914  sinq12ge0  25021  gausslemma2dlem3  25871  2sq2  25936  2sqreultlem  25950  2sqreunnltlem  25953  ax5seglem5  26646  ax5seg  26651  uhgrnbgr0nb  27063  cplgrop  27146  wlkl1loop  27346  uspgr2wlkeq  27354  upgrwlkdvdelem  27444  uhgrwkspthlem2  27462  pthdlem2lem  27475  uspgrn2crct  27513  wlkiswwlks2lem3  27576  wlkiswwlks2  27580  wlkiswwlksupgr2  27582  wlklnwwlkln2lem  27587  wwlksnext  27598  wwlksnextfun  27603  rusgrnumwwlk  27681  clwlkclwwlklem2a4  27702  clwlkclwwlklem3  27706  erclwwlksym  27726  erclwwlknsym  27776  eleclclwwlkn  27782  clwwlknonwwlknonb  27812  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  conngrv2edg  27901  eupth2lem3lem6  27939  frgrncvvdeqlem8  28012  frgrwopreglem4a  28016  frgrreggt1  28099  frgrreg  28100  grpoinveu  28223  ococss  28997  shmodsi  29093  h1datomi  29285  hoaddsub  29520  adjmul  29796  chjatom  30061  atomli  30086  atcvat4i  30101  mdsymlem3  30109  mdsymlem5  30111  mdsymlem6  30112  sumdmdlem  30122  cdj3lem2a  30140  cdj3lem3a  30143  bnj1204  32181  umgr2cycllem  32284  umgr2cycl  32285  cvmsdisj  32414  satfv0fun  32515  satffunlem  32545  satffunlem1lem2  32547  satffunlem2lem2  32550  fundmpss  32906  dfon2lem6  32930  dfon2lem8  32932  frr3g  33018  ifscgr  33402  lineext  33434  fscgr  33438  idinside  33442  btwnconn1lem11  33455  btwnconn1lem12  33456  btwnconn3  33461  brsegle  33466  seglecgr12  33469  hilbert1.2  33513  exp5d  33547  exp5k  33549  nn0prpwlem  33567  bj-restb  34279  exrecfnlem  34542  poimirlem26  34799  poimirlem29  34802  poimirlem32  34805  areacirc  34868  heibor1lem  34968  pridl  35196  pridlc  35230  dmnnzd  35234  prtlem11  35882  prtlem17  35892  ax12indn  35959  atcvrj0  36444  cvrat4  36459  athgt  36472  lplnexllnN  36580  2llnjN  36583  lvolnle3at  36598  lncmp  36799  paddclN  36858  pexmidlem4N  36989  cdleme17d3  37512  cdleme50trn2  37567  cdlemf2  37578  cdlemf  37579  cdlemj3  37839  cdlemk26b-3  37921  dihord5b  38275  isnacs3  39185  jm2.26  39477  sbiota1  40643  exbir  40689  tratrb  40747  onfrALT  40760  in2an  40819  pwtrrVD  41036  suctrALT2VD  41047  suctrALT2  41048  tratrbVD  41072  trintALTVD  41091  trintALT  41092  or2expropbi  43146  2reu8i  43189  2reuimp  43191  zm1nn  43379  2ffzoeq  43405  iccpartiltu  43459  iccpartigtl  43460  iccpartgt  43464  iccpartnel  43475  sbcpr  43560  fmtnofac2lem  43607  fmtnofac2  43608  lighneallem2  43648  odd2prm2  43760  stgoldbwt  43818  sbgoldbst  43820  sbgoldbaltlem1  43821  mogoldbb  43827  isomuspgrlem1  43869  isomuspgrlem2d  43873  lidldomn1  44120  ply1mulgsumlem1  44368  lincsumcl  44414  ellcoellss  44418  islinindfis  44432  lindslinindsimp1  44440  lindslinindsimp2lem5  44445  lindsrng01  44451  elfzolborelfzop1  44502  rrx2linest  44657  aacllem  44830
  Copyright terms: Public domain W3C validator