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

Theorem expd 419
 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 418 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
32com3r 87 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  expcomd  420  exp32  424  exp4b  434  exp4c  436  exp4d  437  exp42  439  exp44  441  exp5c  448  exp5j  449  exp5l  450  pm3.3  452  expdimp  456  impl  459  syland  605  mpan2d  693  a2and  842  3impib  1113  exp5o  1352  ralrimivv  3155  mob2  3654  reuind  3692  reupick3  4240  elpwunsn  4581  disjiun  5017  sotr2  5469  wefrc  5513  relop  5685  predpoirr  6144  predfrirr  6145  fnun  6434  mpteqb  6764  tpres  6940  fconst5  6945  funfvima  6970  riotaeqimp  7119  dfwe2  7476  limuni3  7547  tfisi  7553  ordom  7569  funcnvuni  7618  f1oweALT  7655  frxp  7803  poxp  7805  wfr3g  7936  wfrlem12  7949  onfununi  7961  tz7.48lem  8060  oecl  8145  oaordex  8167  oaass  8170  omwordri  8181  odi  8188  omass  8189  omeu  8194  oen0  8195  oewordi  8200  oewordri  8201  nnarcl  8225  nnmass  8233  dif1en  8735  findcard2  8742  unblem1  8754  unblem2  8755  domunfican  8775  marypha1lem  8881  supiso  8923  inf3lem3  9077  epfrs  9157  karden  9308  infxpenlem  9424  iunfictbso  9525  dfac5  9539  dfac2b  9541  kmlem1  9561  kmlem9  9569  infpssrlem3  9716  fin23lem25  9735  fin23lem30  9753  domtriomlem  9853  axdc3lem4  9864  axcclem  9868  zorn2lem7  9913  konigthlem  9979  wunr1om  10130  tskr1om  10178  gruen  10223  grur1a  10230  indpi  10318  genpnmax  10418  prlem934  10444  ltaddpr  10445  ltexprlem7  10453  ltaprlem  10455  axrrecex  10574  axpre-sup  10580  lelttr  10720  dedekind  10792  addid2  10812  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  12971  elfz0ubfz0  13006  elfzo0z  13074  fzofzim  13079  elfznelfzo  13137  fleqceilz  13217  fsequb  13338  leexp2r  13534  bernneq  13586  fi1uzind  13851  brfi1indALT  13854  swrdnd0  14010  swrdswrdlem  14057  swrdswrd  14058  wrd2ind  14076  swrdccatin1  14078  swrdccatin2  14082  pfxccatin12lem3  14085  repswswrd  14137  cshweqrep  14174  swrd2lsw  14305  2swrd2eqwrdeq  14306  wrdl3s3  14317  s3iunsndisj  14319  cau3lem  14706  climuni  14901  mulcn2  14944  dvdsabseq  15655  divalglem8  15741  ndvdssub  15750  rplpwr  15897  algcvgblem  15911  lcmf  15967  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfdvdsb  15977  lcmfun  15979  euclemma  16047  prmlem1a  16432  setsstruct2  16513  iscatd  16936  initoeu1  17263  initoeu2  17268  termoeu1  17270  plelttr  17574  insubm  17975  grpinveu  18130  cyccom  18338  symgfixelsi  18555  efgred  18866  telgsumfzs  19102  srgmulgass  19274  srgbinom  19288  lspdisjb  19891  mplcoe5lem  20707  cply1mul  20923  coe1fzgsumd  20931  gsummoncoe1  20933  evl1gsumd  20981  cpmatacl  21321  cpmatmcllem  21323  basis2  21556  0ntr  21676  uncmp  22008  1stcrest  22058  txcls  22209  txcnp  22225  tx1stc  22255  fgss2  22479  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  metcnp3  23147  tngngp3  23262  reconn  23433  iscau4  23883  ellimc3  24482  ulmbdd  24993  ulmcn  24994  sinq12ge0  25101  gausslemma2dlem3  25952  2sq2  26017  2sqreultlem  26031  2sqreunnltlem  26034  ax5seglem5  26727  ax5seg  26732  uhgrnbgr0nb  27144  cplgrop  27227  wlkl1loop  27427  uspgr2wlkeq  27435  upgrwlkdvdelem  27525  uhgrwkspthlem2  27543  pthdlem2lem  27556  uspgrn2crct  27594  wlkiswwlks2lem3  27657  wlkiswwlks2  27661  wlkiswwlksupgr2  27663  wlklnwwlkln2lem  27668  wwlksnext  27679  wwlksnextfun  27684  rusgrnumwwlk  27761  clwlkclwwlklem2a4  27782  clwlkclwwlklem3  27786  erclwwlksym  27806  erclwwlknsym  27855  eleclclwwlkn  27861  clwwlknonwwlknonb  27891  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  conngrv2edg  27980  eupth2lem3lem6  28018  frgrncvvdeqlem8  28091  frgrwopreglem4a  28095  frgrreggt1  28178  frgrreg  28179  grpoinveu  28302  ococss  29076  shmodsi  29172  h1datomi  29364  hoaddsub  29599  adjmul  29875  chjatom  30140  atomli  30165  atcvat4i  30180  mdsymlem3  30188  mdsymlem5  30190  mdsymlem6  30191  sumdmdlem  30201  cdj3lem2a  30219  cdj3lem3a  30222  bnj1204  32394  umgr2cycllem  32497  umgr2cycl  32498  cvmsdisj  32627  satfv0fun  32728  satffunlem  32758  satffunlem1lem2  32760  satffunlem2lem2  32763  fundmpss  33119  dfon2lem6  33143  dfon2lem8  33145  frr3g  33231  ifscgr  33615  lineext  33647  fscgr  33651  idinside  33655  btwnconn1lem11  33668  btwnconn1lem12  33669  btwnconn3  33674  brsegle  33679  seglecgr12  33682  hilbert1.2  33726  exp5d  33760  exp5k  33762  nn0prpwlem  33780  bj-restb  34506  exrecfnlem  34793  poimirlem26  35080  poimirlem29  35083  poimirlem32  35086  areacirc  35147  heibor1lem  35244  pridl  35472  pridlc  35506  dmnnzd  35510  prtlem11  36159  prtlem17  36169  ax12indn  36236  atcvrj0  36721  cvrat4  36736  athgt  36749  lplnexllnN  36857  2llnjN  36860  lvolnle3at  36875  lncmp  37076  paddclN  37135  pexmidlem4N  37266  cdleme17d3  37789  cdleme50trn2  37844  cdlemf2  37855  cdlemf  37856  cdlemj3  38116  cdlemk26b-3  38198  dihord5b  38552  isnacs3  39646  jm2.26  39938  sbiota1  41133  exbir  41179  tratrb  41237  onfrALT  41250  in2an  41309  pwtrrVD  41526  suctrALT2VD  41537  suctrALT2  41538  tratrbVD  41562  trintALTVD  41581  trintALT  41582  or2expropbi  43621  2reu8i  43664  2reuimp  43666  zm1nn  43854  2ffzoeq  43880  iccpartiltu  43934  iccpartigtl  43935  iccpartgt  43939  iccpartnel  43950  sbcpr  44033  fmtnofac2lem  44080  fmtnofac2  44081  lighneallem2  44119  odd2prm2  44231  stgoldbwt  44289  sbgoldbst  44291  sbgoldbaltlem1  44292  mogoldbb  44298  isomuspgrlem1  44340  isomuspgrlem2d  44344  lidldomn1  44540  ply1mulgsumlem1  44789  lincsumcl  44835  ellcoellss  44839  islinindfis  44853  lindslinindsimp1  44861  lindslinindsimp2lem5  44866  lindsrng01  44872  elfzolborelfzop1  44923  rrx2linest  45151  aacllem  45324
 Copyright terms: Public domain W3C validator