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  1600  cbv1  2303  ralimdva  2991  reuss2  3940  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  funfvima2  6533  isofrlem  6630  dfwe2  7023  tfindsg  7102  tfinds2  7105  tfinds3  7106  ordom  7116  findsg  7135  finds2  7136  wfr3g  7458  tfrlem1  7517  tfr3  7540  tz7.48lem  7581  oaordi  7671  oeordi  7712  nnaordi  7743  nnawordi  7746  nneneq  8184  ac6sfi  8245  domunfican  8274  fodomfi  8280  finsschain  8314  marypha1lem  8380  inf3lem2  8564  inf3lem5  8567  cantnfval2  8604  cantnflt  8607  cantnfp1lem3  8615  cnfcom  8635  dfac12lem3  9005  ackbij1lem16  9095  sornom  9137  infpssrlem4  9166  fin23lem34  9206  fin23lem36  9208  isf32lem1  9213  isf32lem2  9214  zorn2lem4  9359  zorn2lem5  9360  zorn2lem6  9361  zorn2lem7  9362  ttukeylem5  9373  pwfseqlem3  9520  wunfi  9581  grudomon  9677  prlem934  9893  sup2  11017  nnaddcl  11080  nnmulcl  11081  peano5uzi  11504  uzind2  11508  nn0indd  11512  fzind  11513  zindd  11516  uzaddcl  11782  uzwo  11789  om2uzlti  12789  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqcaopr3  12876  seqf1olem2a  12879  seqf1o  12882  seqid2  12887  seqhomo  12888  ser1const  12897  expcllem  12911  expeq0  12930  mulexp  12939  expadd  12942  expmul  12945  leexp2r  12958  leexp1a  12959  bernneq  13030  modexp  13039  facdiv  13114  facwordi  13116  faclbnd  13117  faclbnd4lem4  13123  faclbnd6  13126  hashgadd  13204  hashmap  13260  hashf1lem2  13278  hashf1  13279  seqcoll  13286  cshweqrep  13613  relexpsucnnl  13816  relexpcnv  13819  relexpnndm  13825  relexpaddnn  13835  cjexp  13934  absexp  14088  rlimsqzlem  14423  lo1le  14426  iseraltlem2  14457  fsum2d  14546  modfsummod  14570  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  binom  14606  bcxmas  14611  climcndslem1  14625  climcndslem2  14626  cvgrat  14659  clim2prod  14664  prodfn0  14670  prodfrec  14671  ntrivcvgfvn0  14675  fprodabs  14748  fprod2d  14755  binomfallfac  14816  bpolycl  14827  fprodefsum  14869  demoivreALT  14975  ruclem8  15010  ruclem9  15011  dvdsfac  15095  bitsinv1  15211  sadcadd  15227  sadadd2  15229  saddisjlem  15233  smuval2  15251  smupvallem  15252  smu01lem  15254  smupval  15257  smueqlem  15259  smumullem  15261  gcdmultiple  15316  rplpwr  15323  nn0seqcvgd  15330  seq1st  15331  alginv  15335  algcvga  15339  algfx  15340  prmdvdsexp  15474  prmfac1  15478  eulerthlem2  15534  pcmpt  15643  pcfac  15650  prmpwdvds  15655  prmreclem4  15670  vdwlem10  15741  ramcl  15780  mreexexd  16355  mreexexdOLD  16356  frmdgsum  17446  mulgnnass  17623  mulgnnassOLD  17624  mhmmulg  17630  gsumwrev  17842  gsmsymgrfix  17894  gsmsymgreq  17898  sylow1lem1  18059  efginvrel2  18186  efgsrel  18193  gsum2dlem2  18416  ablfac1eulem  18517  pgpfac  18529  srgmulgass  18577  srgpcomp  18578  srgbinom  18591  lmodvsmmulgdi  18946  assamulgscm  19398  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  mptcoe1fsupp  19633  coe1fzgsumdlem  19719  coe1fzgsumd  19720  gsummoncoe1  19722  evl1gsumdlem  19768  evl1gsumd  19769  cnfldexp  19827  mdetunilem9  20474  mptcoe1matfsupp  20655  mp2pm2mplem4  20662  chpdmat  20694  tgcl  20821  fiuncmp  21255  2ndcsep  21310  1stcelcls  21312  ptcmpfi  21664  tmdmulg  21943  tmdgsum  21946  imasdsf1olem  22225  fsumcn  22720  caubl  23152  caublcls  23153  ovolunlem1a  23310  ovolfiniun  23315  ovolicc2lem3  23333  volfiniun  23361  voliunlem1  23364  volsuplem  23369  volsup  23370  dyadmax  23412  itgfsum  23638  dvnadd  23737  dvnres  23739  cpnord  23743  dvnfre  23760  dvmptfsum  23783  ply1divex  23941  fta1g  23972  plyco  24042  dgrcolem1  24074  dgrco  24076  dvnply2  24087  plydivex  24097  aaliou3lem2  24143  dvntaylp  24170  taylthlem1  24172  cxpmul2  24480  jensen  24760  ftalem2  24845  bcmono  25047  bposlem5  25058  lgsquad2lem2  25155  dchrisumlem1  25223  dchrisum0flb  25244  pntpbnd1  25320  pntlemf  25339  qabvle  25359  qabvexp  25360  ostthlem2  25362  ostth2lem2  25368  rusgrnumwwlk  26942  eupth2lems  27216  eupth2  27217  ipasslem1  27814  mdslmd1lem1  29312  mdslmd1lem2  29313  iuninc  29505  ssrelf  29553  nnindd  29694  nn0min  29695  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  ofldchr  29942  cmppcmp  30053  nexple  30199  esumfzf  30259  sseqp1  30585  rrvsum  30644  signstfvc  30779  bnj1174  31197  subfacp1lem6  31293  cvmliftlem7  31399  cvmliftlem10  31402  mrsubvrs  31545  bccolsum  31751  iprodefisumlem  31752  faclimlem1  31755  trpredmintr  31855  frr3g  31904  nosupbnd1lem5  31983  onsuct0  32565  findfvcl  32576  bj-imim2ALT  32663  bj-cbv1v  32854  poimirlem28  33567  sdclem2  33668  seqpo  33673  incsequz  33674  mettrifi  33683  heiborlem4  33743  bfplem1  33751  pclfinclN  35554  incssnn0  37591  mzpexpmpt  37625  pell14qrexpclnn0  37747  monotuz  37823  expmordi  37829  rmxypos  37831  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  jm2.18  37872  jm2.19lem3  37875  jm2.15nn0  37887  jm2.16nn0  37888  dfac11  37949  pwslnm  37981  hbtlem5  38015  cnsrexpcl  38052  relexpxpnnidm  38312  relexpiidm  38313  relexpss1d  38314  iunrelexpmin1  38317  relexpmulnn  38318  iunrelexpmin2  38321  relexp0a  38325  trclimalb2  38335  dvgrat  38828  monoordxrv  40025  smonoord  41666  lmodvsmdi  42488  tfis2d  42752
  Copyright terms: Public domain W3C validator