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  1558  cbv1  2265  ralimdva  2959  reuss2  3899  ssrel  5197  ssrelOLD  5198  ssrel2  5200  ssrelrel  5210  funfvima2  6478  isofrlem  6575  dfwe2  6966  tfindsg  7045  tfinds2  7048  tfinds3  7049  ordom  7059  findsg  7078  finds2  7079  wfr3g  7398  tfrlem1  7457  tfr3  7480  tz7.48lem  7521  oaordi  7611  oeordi  7652  nnaordi  7683  nnawordi  7686  nneneq  8128  ac6sfi  8189  domunfican  8218  fodomfi  8224  finsschain  8258  marypha1lem  8324  inf3lem2  8511  inf3lem5  8514  cantnfval2  8551  cantnflt  8554  cantnfp1lem3  8562  cnfcom  8582  dfac12lem3  8952  ackbij1lem16  9042  sornom  9084  infpssrlem4  9113  fin23lem34  9153  fin23lem36  9155  isf32lem1  9160  isf32lem2  9161  zorn2lem4  9306  zorn2lem5  9307  zorn2lem6  9308  zorn2lem7  9309  ttukeylem5  9320  pwfseqlem3  9467  wunfi  9528  grudomon  9624  prlem934  9840  sup2  10964  nnaddcl  11027  nnmulcl  11028  peano5uzi  11451  uzind2  11455  nn0indd  11459  fzind  11460  zindd  11463  uzaddcl  11729  uzwo  11736  om2uzlti  12732  seqcl2  12802  seqfveq2  12806  seqshft2  12810  monoord  12814  seqsplit  12817  seqcaopr3  12819  seqf1olem2a  12822  seqf1o  12825  seqid2  12830  seqhomo  12831  ser1const  12840  expcllem  12854  expeq0  12873  mulexp  12882  expadd  12885  expmul  12888  leexp2r  12901  leexp1a  12902  bernneq  12973  modexp  12982  facdiv  13057  facwordi  13059  faclbnd  13060  faclbnd4lem4  13066  faclbnd6  13069  hashgadd  13149  hashmap  13205  hashf1lem2  13223  hashf1  13224  seqcoll  13231  cshweqrep  13548  relexpsucnnl  13753  relexpcnv  13756  relexpnndm  13762  relexpaddnn  13772  cjexp  13871  absexp  14025  rlimsqzlem  14360  lo1le  14363  iseraltlem2  14394  fsum2d  14483  modfsummod  14507  fsumabs  14514  fsumrlim  14524  fsumo1  14525  fsumiun  14534  binom  14543  bcxmas  14548  climcndslem1  14562  climcndslem2  14563  cvgrat  14596  clim2prod  14601  prodfn0  14607  prodfrec  14608  ntrivcvgfvn0  14612  fprodabs  14685  fprod2d  14692  binomfallfac  14753  bpolycl  14764  fprodefsum  14806  demoivreALT  14912  ruclem8  14947  ruclem9  14948  dvdsfac  15029  bitsinv1  15145  sadcadd  15161  sadadd2  15163  saddisjlem  15167  smuval2  15185  smupvallem  15186  smu01lem  15188  smupval  15191  smueqlem  15193  smumullem  15195  gcdmultiple  15250  rplpwr  15257  nn0seqcvgd  15264  seq1st  15265  alginv  15269  algcvga  15273  algfx  15274  prmdvdsexp  15408  prmfac1  15412  eulerthlem2  15468  pcmpt  15577  pcfac  15584  prmpwdvds  15589  prmreclem4  15604  vdwlem10  15675  ramcl  15714  mreexexd  16289  mreexexdOLD  16290  frmdgsum  17380  mulgnnass  17557  mulgnnassOLD  17558  mhmmulg  17564  gsumwrev  17777  gsmsymgrfix  17829  gsmsymgreq  17833  sylow1lem1  17994  efginvrel2  18121  efgsrel  18128  gsum2dlem2  18351  ablfac1eulem  18452  pgpfac  18464  srgmulgass  18512  srgpcomp  18513  srgbinom  18526  lmodvsmmulgdi  18879  assamulgscm  19331  mplcoe1  19446  mplcoe3  19447  mplcoe5  19449  mptcoe1fsupp  19566  coe1fzgsumdlem  19652  coe1fzgsumd  19653  gsummoncoe1  19655  evl1gsumdlem  19701  evl1gsumd  19702  cnfldexp  19760  mdetunilem9  20407  mptcoe1matfsupp  20588  mp2pm2mplem4  20595  chpdmat  20627  tgcl  20754  fiuncmp  21188  2ndcsep  21243  1stcelcls  21245  ptcmpfi  21597  tmdmulg  21877  tmdgsum  21880  imasdsf1olem  22159  fsumcn  22654  caubl  23087  caublcls  23088  ovolunlem1a  23245  ovolfiniun  23250  ovolicc2lem3  23268  volfiniun  23296  voliunlem1  23299  volsuplem  23304  volsup  23305  dyadmax  23347  itgfsum  23574  dvnadd  23673  dvnres  23675  cpnord  23679  dvnfre  23696  dvmptfsum  23719  ply1divex  23877  fta1g  23908  plyco  23978  dgrcolem1  24010  dgrco  24012  dvnply2  24023  plydivex  24033  aaliou3lem2  24079  dvntaylp  24106  taylthlem1  24108  cxpmul2  24416  jensen  24696  ftalem2  24781  bcmono  24983  bposlem5  24994  lgsquad2lem2  25091  dchrisumlem1  25159  dchrisum0flb  25180  pntpbnd1  25256  pntlemf  25275  qabvle  25295  qabvexp  25296  ostthlem2  25298  ostth2lem2  25304  rusgrnumwwlk  26851  eupth2lems  27078  eupth2  27079  ipasslem1  27656  mdslmd1lem1  29154  mdslmd1lem2  29155  iuninc  29351  ssrelf  29397  nnindd  29540  nn0min  29541  gsumle  29753  gsumvsca1  29756  gsumvsca2  29757  ofldchr  29788  cmppcmp  29899  nexple  30045  esumfzf  30105  sseqp1  30431  rrvsum  30490  signstfvc  30625  bnj1174  31045  subfacp1lem6  31141  cvmliftlem7  31247  cvmliftlem10  31250  mrsubvrs  31393  bccolsum  31600  iprodefisumlem  31601  faclimlem1  31604  trpredmintr  31705  frr3g  31753  nosupbnd1lem5  31832  onsuct0  32415  findfvcl  32426  bj-imim2ALT  32513  bj-cbv1v  32704  poimirlem28  33408  sdclem2  33509  seqpo  33514  incsequz  33515  mettrifi  33524  heiborlem4  33584  bfplem1  33592  pclfinclN  35055  incssnn0  37093  mzpexpmpt  37127  pell14qrexpclnn0  37249  monotuz  37325  expmordi  37331  rmxypos  37333  jm2.17a  37346  jm2.17b  37347  rmygeid  37350  jm2.18  37374  jm2.19lem3  37377  jm2.15nn0  37389  jm2.16nn0  37390  dfac11  37451  pwslnm  37483  hbtlem5  37517  cnsrexpcl  37554  relexpxpnnidm  37814  relexpiidm  37815  relexpss1d  37816  iunrelexpmin1  37819  relexpmulnn  37820  iunrelexpmin2  37823  relexp0a  37827  trclimalb2  37837  dvgrat  38331  smonoord  41105  lmodvsmdi  41928  tfis2d  42192
  Copyright terms: Public domain W3C validator