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  843  minimp  1623  cbv1v  2348  cbv1  2414  ralimdva  3147  reuss2  4238  ssrel  5625  ssrel2  5627  ssrelrel  5637  funfvima2  6975  isofrlem  7076  dfwe2  7480  tfindsg  7559  tfinds2  7562  tfinds3  7563  ordom  7573  findsg  7594  finds2  7595  wfr3g  7940  tfrlem1  7999  tfr3  8022  tz7.48lem  8064  oaordi  8159  oeordi  8200  nnaordi  8231  nnawordi  8234  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  9560  ackbij1lem16  9650  sornom  9692  infpssrlem4  9721  fin23lem34  9761  fin23lem36  9763  isf32lem1  9768  isf32lem2  9769  zorn2lem4  9914  zorn2lem5  9915  zorn2lem6  9916  zorn2lem7  9917  ttukeylem5  9928  pwfseqlem3  10075  wunfi  10136  grudomon  10232  prlem934  10448  sup2  11588  nnindd  11649  nnaddcl  11652  nnmulcl  11653  nnne0  11663  peano5uzi  12063  uzind2  12067  nn0indd  12071  fzind  12072  zindd  12075  uzaddcl  12296  uzwo  12303  om2uzlti  13317  seqcaopr3  13405  seqf1olem2a  13408  seqf1o  13411  ser1const  13426  expcllem  13440  expeq0  13459  mulexp  13468  expadd  13471  expmul  13474  expmordi  13531  leexp2r  13538  leexp1a  13539  bernneq  13590  modexp  13599  facdiv  13647  facwordi  13649  faclbnd  13650  faclbnd4lem4  13656  hashgadd  13738  hashmap  13796  hashf1lem2  13814  hashf1  13815  seqcoll  13822  cshweqrep  14178  relexpsucnnl  14386  relexpcnv  14389  relexpnndm  14395  relexpaddnn  14405  rlimsqzlem  15000  lo1le  15003  iseraltlem2  15034  fsum2d  15121  modfsummod  15144  fsumabs  15151  fsumrlim  15161  fsumo1  15162  fsumiun  15171  binom  15180  climcndslem1  15199  climcndslem2  15200  cvgrat  15234  clim2prod  15239  prodfn0  15245  prodfrec  15246  ntrivcvgfvn0  15250  fprodabs  15323  fprod2d  15330  binomfallfac  15390  bpolycl  15401  fprodefsum  15443  demoivreALT  15549  ruclem8  15585  ruclem9  15586  dvdsfac  15671  bitsinv1  15784  sadcadd  15800  sadadd2  15802  saddisjlem  15806  smuval2  15824  smupvallem  15825  smu01lem  15827  smupval  15830  smueqlem  15832  smumullem  15834  gcdmultipleOLD  15893  rplpwr  15900  nn0seqcvgd  15907  seq1st  15908  alginv  15912  algcvga  15916  algfx  15917  prmdvdsexp  16052  prmfac1  16056  eulerthlem2  16112  pcmpt  16221  pcfac  16228  prmpwdvds  16233  prmreclem4  16248  vdwlem10  16319  ramcl  16358  mreexexd  16914  frmdgsum  18022  mulgnnass  18257  mhmmulg  18263  gsumwrev  18489  gsmsymgrfix  18551  gsmsymgreq  18555  efginvrel2  18848  efgsrel  18855  gsum2dlem2  19087  ablfac1eulem  19190  pgpfac  19202  srgmulgass  19277  srgpcomp  19278  srgbinom  19291  lmodvsmmulgdi  19665  cnfldexp  20127  assamulgscm  20590  mplcoe1  20708  mplcoe3  20709  mplcoe5  20711  mptcoe1fsupp  20847  coe1fzgsumdlem  20933  coe1fzgsumd  20934  gsummoncoe1  20936  evl1gsumdlem  20983  evl1gsumd  20984  mdetunilem9  21228  mptcoe1matfsupp  21410  mp2pm2mplem4  21417  chpdmat  21449  tgcl  21577  fiuncmp  22012  2ndcsep  22067  1stcelcls  22069  ptcmpfi  22421  tmdgsum  22703  fsumcn  23478  caubl  23915  caublcls  23916  ovolunlem1a  24103  ovolfiniun  24108  volfiniun  24154  voliunlem1  24157  volsuplem  24162  volsup  24163  dyadmax  24205  itgfsum  24433  dvnadd  24535  cpnord  24541  dvnfre  24558  dvmptfsum  24581  ply1divex  24740  fta1g  24771  plyco  24841  dgrcolem1  24873  dgrco  24875  dvnply2  24886  plydivex  24896  aaliou3lem2  24942  dvntaylp  24969  taylthlem1  24971  cxpmul2  25283  jensen  25577  ftalem2  25662  bcmono  25864  bposlem5  25875  lgsquad2lem2  25972  dchrisumlem1  26076  dchrisum0flb  26097  pntpbnd1  26173  pntlemf  26192  qabvle  26212  qabvexp  26213  ostthlem2  26215  ostth2lem2  26221  rusgrnumwwlk  27764  eupth2lems  28026  eupth2  28027  ipasslem1  28617  mdslmd1lem1  30111  mdslmd1lem2  30112  iuninc  30327  ssrelf  30382  nn0min  30565  gsumle  30778  gsumvsca1  30907  gsumvsca2  30908  ofldchr  30941  cmppcmp  31211  nexple  31376  esumfzf  31436  sseqp1  31761  rrvsum  31820  signstfvc  31952  bnj1174  32383  lfuhgr2  32473  subfacp1lem6  32540  mrsubvrs  32877  bccolsum  33079  iprodefisumlem  33080  faclimlem1  33083  trpredmintr  33178  frr3g  33229  fpr3g  33230  nosupbnd1lem5  33320  onsuct0  33897  findfvcl  33908  poimirlem28  35078  sdclem2  35173  seqpo  35178  incsequz  35179  mettrifi  35188  heiborlem4  35245  bfplem1  35253  pclfinclN  37239  fzindd  39256  uzindd  39257  nnaddcom  39456  nnadddir  39458  nnmulcom  39460  sn-sup2  39581  incssnn0  39639  mzpexpmpt  39673  pell14qrexpclnn0  39794  monotuz  39869  rmxypos  39875  jm2.17a  39888  jm2.17b  39889  rmygeid  39892  jm2.18  39916  jm2.19lem3  39919  jm2.15nn0  39931  jm2.16nn0  39932  dfac11  39993  pwslnm  40025  hbtlem5  40059  cnsrexpcl  40096  relexpxpnnidm  40391  relexpiidm  40392  relexpss1d  40393  iunrelexpmin1  40396  relexpmulnn  40397  iunrelexpmin2  40400  relexp0a  40404  trclimalb2  40414  dvgrat  41003  lmodvsmdi  44771  tfis2d  45197
  Copyright terms: Public domain W3C validator