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

Theorem a2d 29
Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 7. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
a2d (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 ax-2 7 . 2 ((𝜓 → (𝜒𝜃)) → ((𝜓𝜒) → (𝜓𝜃)))
31, 2syl 17 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpdd  43  imim2d  57  imim3i  64  loowoz  111  minimp  1709  cbv1  2412  ralimdva  3100  reuss2  4050  ssrel  5364  ssrelOLD  5365  ssrel2  5367  ssrelrel  5377  funfvima2  6656  isofrlem  6753  dfwe2  7146  tfindsg  7225  tfinds2  7228  tfinds3  7229  ordom  7239  findsg  7258  finds2  7259  wfr3g  7582  tfrlem1  7641  tfr3  7664  tz7.48lem  7705  oaordi  7795  oeordi  7836  nnaordi  7867  nnawordi  7870  nneneq  8308  ac6sfi  8369  domunfican  8398  fodomfi  8404  finsschain  8438  marypha1lem  8504  inf3lem2  8699  inf3lem5  8702  cantnfval2  8739  cantnflt  8742  cantnfp1lem3  8750  cnfcom  8770  dfac12lem3  9159  ackbij1lem16  9249  sornom  9291  infpssrlem4  9320  fin23lem34  9360  fin23lem36  9362  isf32lem1  9367  isf32lem2  9368  zorn2lem4  9513  zorn2lem5  9514  zorn2lem6  9515  zorn2lem7  9516  ttukeylem5  9527  pwfseqlem3  9674  wunfi  9735  grudomon  9831  prlem934  10047  sup2  11171  nnaddcl  11234  nnmulcl  11235  peano5uzi  11658  uzind2  11662  nn0indd  11666  fzind  11667  zindd  11670  uzaddcl  11937  uzwo  11944  om2uzlti  12943  seqcl2  13013  seqfveq2  13017  seqshft2  13021  monoord  13025  seqsplit  13028  seqcaopr3  13030  seqf1olem2a  13033  seqf1o  13036  seqid2  13041  seqhomo  13042  ser1const  13051  expcllem  13065  expeq0  13084  mulexp  13093  expadd  13096  expmul  13099  leexp2r  13112  leexp1a  13113  bernneq  13184  modexp  13193  facdiv  13268  facwordi  13270  faclbnd  13271  faclbnd4lem4  13277  faclbnd6  13280  hashgadd  13358  hashmap  13414  hashf1lem2  13432  hashf1  13433  seqcoll  13440  cshweqrep  13767  relexpsucnnl  13971  relexpcnv  13974  relexpnndm  13980  relexpaddnn  13990  cjexp  14089  absexp  14243  rlimsqzlem  14578  lo1le  14581  iseraltlem2  14612  fsum2d  14701  modfsummod  14725  fsumabs  14732  fsumrlim  14742  fsumo1  14743  fsumiun  14752  binom  14761  bcxmas  14766  climcndslem1  14780  climcndslem2  14781  cvgrat  14814  clim2prod  14819  prodfn0  14825  prodfrec  14826  ntrivcvgfvn0  14830  fprodabs  14903  fprod2d  14910  binomfallfac  14971  bpolycl  14982  fprodefsum  15024  demoivreALT  15130  ruclem8  15165  ruclem9  15166  dvdsfac  15250  bitsinv1  15366  sadcadd  15382  sadadd2  15384  saddisjlem  15388  smuval2  15406  smupvallem  15407  smu01lem  15409  smupval  15412  smueqlem  15414  smumullem  15416  gcdmultiple  15471  rplpwr  15478  nn0seqcvgd  15485  seq1st  15486  alginv  15490  algcvga  15494  algfx  15495  prmdvdsexp  15629  prmfac1  15633  eulerthlem2  15689  pcmpt  15798  pcfac  15805  prmpwdvds  15810  prmreclem4  15825  vdwlem10  15896  ramcl  15935  mreexexd  16510  frmdgsum  17600  mulgnnass  17777  mulgnnassOLD  17778  mhmmulg  17784  gsumwrev  17996  gsmsymgrfix  18048  gsmsymgreq  18052  sylow1lem1  18213  efginvrel2  18340  efgsrel  18347  gsum2dlem2  18570  ablfac1eulem  18671  pgpfac  18683  srgmulgass  18731  srgpcomp  18732  srgbinom  18745  lmodvsmmulgdi  19100  assamulgscm  19552  mplcoe1  19667  mplcoe3  19668  mplcoe5  19670  mptcoe1fsupp  19787  coe1fzgsumdlem  19873  coe1fzgsumd  19874  gsummoncoe1  19876  evl1gsumdlem  19922  evl1gsumd  19923  cnfldexp  19981  mdetunilem9  20628  mptcoe1matfsupp  20809  mp2pm2mplem4  20816  chpdmat  20848  tgcl  20975  fiuncmp  21409  2ndcsep  21464  1stcelcls  21466  ptcmpfi  21818  tmdmulg  22097  tmdgsum  22100  imasdsf1olem  22379  fsumcn  22874  caubl  23306  caublcls  23307  ovolunlem1a  23464  ovolfiniun  23469  ovolicc2lem3  23487  volfiniun  23515  voliunlem1  23518  volsuplem  23523  volsup  23524  dyadmax  23566  itgfsum  23792  dvnadd  23891  dvnres  23893  cpnord  23897  dvnfre  23914  dvmptfsum  23937  ply1divex  24095  fta1g  24126  plyco  24196  dgrcolem1  24228  dgrco  24230  dvnply2  24241  plydivex  24251  aaliou3lem2  24297  dvntaylp  24324  taylthlem1  24326  cxpmul2  24634  jensen  24914  ftalem2  24999  bcmono  25201  bposlem5  25212  lgsquad2lem2  25309  dchrisumlem1  25377  dchrisum0flb  25398  pntpbnd1  25474  pntlemf  25493  qabvle  25513  qabvexp  25514  ostthlem2  25516  ostth2lem2  25522  rusgrnumwwlk  27097  eupth2lems  27390  eupth2  27391  ipasslem1  27995  mdslmd1lem1  29493  mdslmd1lem2  29494  iuninc  29686  ssrelf  29734  nnindd  29875  nn0min  29876  gsumle  30088  gsumvsca1  30091  gsumvsca2  30092  ofldchr  30123  cmppcmp  30234  nexple  30380  esumfzf  30440  sseqp1  30766  rrvsum  30825  signstfvc  30960  bnj1174  31378  subfacp1lem6  31474  cvmliftlem7  31580  cvmliftlem10  31583  mrsubvrs  31726  bccolsum  31932  iprodefisumlem  31933  faclimlem1  31936  trpredmintr  32036  frr3g  32085  nosupbnd1lem5  32164  onsuct0  32746  findfvcl  32757  bj-imim2ALT  32844  bj-cbv1v  33035  poimirlem28  33750  sdclem2  33851  seqpo  33856  incsequz  33857  mettrifi  33866  heiborlem4  33926  bfplem1  33934  pclfinclN  35739  incssnn0  37776  mzpexpmpt  37810  pell14qrexpclnn0  37932  monotuz  38008  expmordi  38014  rmxypos  38016  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  jm2.18  38057  jm2.19lem3  38060  jm2.15nn0  38072  jm2.16nn0  38073  dfac11  38134  pwslnm  38166  hbtlem5  38200  cnsrexpcl  38237  relexpxpnnidm  38497  relexpiidm  38498  relexpss1d  38499  iunrelexpmin1  38502  relexpmulnn  38503  iunrelexpmin2  38506  relexp0a  38510  trclimalb2  38520  dvgrat  39013  monoordxrv  40210  smonoord  41851  lmodvsmdi  42673  tfis2d  42937
  Copyright terms: Public domain W3C validator