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  112  animpimp2impd  840  minimp  1613  cbv1v  2347  cbv1  2413  ralimdva  3174  reuss2  4280  ssrel  5650  ssrel2  5652  ssrelrel  5662  funfvima2  6984  isofrlem  7082  dfwe2  7485  tfindsg  7564  tfinds2  7567  tfinds3  7568  ordom  7578  findsg  7598  finds2  7599  wfr3g  7942  tfrlem1  8001  tfr3  8024  tz7.48lem  8066  oaordi  8161  oeordi  8202  nnaordi  8233  nnawordi  8236  nneneq  8688  ac6sfi  8750  domunfican  8779  fodomfi  8785  finsschain  8819  marypha1lem  8885  inf3lem2  9080  inf3lem5  9083  cantnfval2  9120  cantnflt  9123  cantnfp1lem3  9131  cnfcom  9151  dfac12lem3  9559  ackbij1lem16  9645  sornom  9687  infpssrlem4  9716  fin23lem34  9756  fin23lem36  9758  isf32lem1  9763  isf32lem2  9764  zorn2lem4  9909  zorn2lem5  9910  zorn2lem6  9911  zorn2lem7  9912  ttukeylem5  9923  pwfseqlem3  10070  wunfi  10131  grudomon  10227  prlem934  10443  sup2  11585  nnaddcl  11648  nnmulcl  11649  nnne0  11659  peano5uzi  12059  uzind2  12063  nn0indd  12067  fzind  12068  zindd  12071  uzaddcl  12292  uzwo  12299  om2uzlti  13306  seqcaopr3  13393  seqf1olem2a  13396  seqf1o  13399  ser1const  13414  expcllem  13428  expeq0  13447  mulexp  13456  expadd  13459  expmul  13462  expmordi  13519  leexp2r  13526  leexp1a  13527  bernneq  13578  modexp  13587  facdiv  13635  facwordi  13637  faclbnd  13638  faclbnd4lem4  13644  hashgadd  13726  hashmap  13784  hashf1lem2  13802  hashf1  13803  seqcoll  13810  cshweqrep  14171  relexpsucnnl  14379  relexpcnv  14382  relexpnndm  14388  relexpaddnn  14398  rlimsqzlem  14993  lo1le  14996  iseraltlem2  15027  fsum2d  15114  modfsummod  15137  fsumabs  15144  fsumrlim  15154  fsumo1  15155  fsumiun  15164  binom  15173  climcndslem1  15192  climcndslem2  15193  cvgrat  15227  clim2prod  15232  prodfn0  15238  prodfrec  15239  ntrivcvgfvn0  15243  fprodabs  15316  fprod2d  15323  binomfallfac  15383  bpolycl  15394  fprodefsum  15436  demoivreALT  15542  ruclem8  15578  ruclem9  15579  dvdsfac  15664  bitsinv1  15779  sadcadd  15795  sadadd2  15797  saddisjlem  15801  smuval2  15819  smupvallem  15820  smu01lem  15822  smupval  15825  smueqlem  15827  smumullem  15829  gcdmultipleOLD  15888  rplpwr  15895  nn0seqcvgd  15902  seq1st  15903  alginv  15907  algcvga  15911  algfx  15912  prmdvdsexp  16047  prmfac1  16051  eulerthlem2  16107  pcmpt  16216  pcfac  16223  prmpwdvds  16228  prmreclem4  16243  vdwlem10  16314  ramcl  16353  mreexexd  16907  frmdgsum  18015  mulgnnass  18200  mhmmulg  18206  gsumwrev  18432  gsmsymgrfix  18485  gsmsymgreq  18489  efginvrel2  18782  efgsrel  18789  gsum2dlem2  19020  ablfac1eulem  19123  pgpfac  19135  srgmulgass  19210  srgpcomp  19211  srgbinom  19224  lmodvsmmulgdi  19598  assamulgscm  20058  mplcoe1  20174  mplcoe3  20175  mplcoe5  20177  mptcoe1fsupp  20311  coe1fzgsumdlem  20397  coe1fzgsumd  20398  gsummoncoe1  20400  evl1gsumdlem  20447  evl1gsumd  20448  cnfldexp  20506  mdetunilem9  21157  mptcoe1matfsupp  21338  mp2pm2mplem4  21345  chpdmat  21377  tgcl  21505  fiuncmp  21940  2ndcsep  21995  1stcelcls  21997  ptcmpfi  22349  tmdgsum  22631  fsumcn  23405  caubl  23838  caublcls  23839  ovolunlem1a  24024  ovolfiniun  24029  volfiniun  24075  voliunlem1  24078  volsuplem  24083  volsup  24084  dyadmax  24126  itgfsum  24354  dvnadd  24453  cpnord  24459  dvnfre  24476  dvmptfsum  24499  ply1divex  24657  fta1g  24688  plyco  24758  dgrcolem1  24790  dgrco  24792  dvnply2  24803  plydivex  24813  aaliou3lem2  24859  dvntaylp  24886  taylthlem1  24888  cxpmul2  25199  jensen  25493  ftalem2  25578  bcmono  25780  bposlem5  25791  lgsquad2lem2  25888  dchrisumlem1  25992  dchrisum0flb  26013  pntpbnd1  26089  pntlemf  26108  qabvle  26128  qabvexp  26129  ostthlem2  26131  ostth2lem2  26137  rusgrnumwwlk  27681  eupth2lems  27944  eupth2  27945  ipasslem1  28535  mdslmd1lem1  30029  mdslmd1lem2  30030  iuninc  30240  ssrelf  30294  nnindd  30462  nn0min  30463  gsumle  30652  gsumvsca1  30781  gsumvsca2  30782  ofldchr  30814  cmppcmp  31021  nexple  31167  esumfzf  31227  sseqp1  31552  rrvsum  31611  signstfvc  31743  bnj1174  32172  lfuhgr2  32262  subfacp1lem6  32329  mrsubvrs  32666  bccolsum  32868  iprodefisumlem  32869  faclimlem1  32872  trpredmintr  32967  frr3g  33018  fpr3g  33019  nosupbnd1lem5  33109  onsuct0  33686  findfvcl  33697  poimirlem28  34801  sdclem2  34898  seqpo  34903  incsequz  34904  mettrifi  34913  heiborlem4  34973  bfplem1  34981  pclfinclN  36966  nnaddcom  39039  nnadddir  39041  nnmulcom  39043  incssnn0  39186  mzpexpmpt  39220  pell14qrexpclnn0  39341  monotuz  39416  rmxypos  39422  jm2.17a  39435  jm2.17b  39436  rmygeid  39439  jm2.18  39463  jm2.19lem3  39466  jm2.15nn0  39478  jm2.16nn0  39479  dfac11  39540  pwslnm  39572  hbtlem5  39606  cnsrexpcl  39643  relexpxpnnidm  39926  relexpiidm  39927  relexpss1d  39928  iunrelexpmin1  39931  relexpmulnn  39932  iunrelexpmin2  39935  relexp0a  39939  trclimalb2  39949  dvgrat  40521  lmodvsmdi  44358  tfis2d  44711
  Copyright terms: Public domain W3C validator