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  845  minimp  1624  cbv1v  2333  cbv1  2401  ralimdva  3161  reuss2  4276  ssrel  5739  ssrelOLD  5740  ssrel2  5742  ssrelrel  5753  funfvima2  7182  isofrlem  7286  dfwe2  7709  tfindsg  7798  tfinds2  7801  tfinds3  7802  trom  7812  findsg  7837  finds2  7838  xpord3inddlem  8087  fpr3g  8217  wfr3g  8254  tfrlem1  8323  tfr3  8346  tz7.48lem  8388  oaordi  8494  oeordi  8535  nnaordi  8566  nnawordi  8569  naddssim  8632  nneneq  9156  nneneqOLD  9168  ac6sfi  9234  domunfican  9267  fodomfi  9272  finsschain  9306  marypha1lem  9374  inf3lem2  9570  inf3lem5  9573  cantnfval2  9610  cantnflt  9613  cantnfp1lem3  9621  cnfcom  9641  ttrclss  9661  ttrclselem2  9667  frr3g  9697  dfac12lem3  10086  ackbij1lem16  10176  sornom  10218  infpssrlem4  10247  fin23lem34  10287  fin23lem36  10289  isf32lem1  10294  isf32lem2  10295  zorn2lem4  10440  zorn2lem5  10441  zorn2lem6  10442  zorn2lem7  10443  ttukeylem5  10454  pwfseqlem3  10601  wunfi  10662  grudomon  10758  prlem934  10974  sup2  12116  nnindd  12178  nnaddcl  12181  nnmulcl  12182  nnne0  12192  peano5uzi  12597  uzind2  12601  nn0indd  12605  fzind  12606  zindd  12609  fzindd  12610  uzaddcl  12834  uzwo  12841  om2uzlti  13861  seqcaopr3  13949  seqf1olem2a  13952  seqf1o  13955  ser1const  13970  expcllem  13984  expeq0  14004  mulexp  14013  expadd  14016  expmul  14019  expmordi  14078  leexp2r  14085  leexp1a  14086  bernneq  14138  modexp  14147  facdiv  14193  facwordi  14195  faclbnd  14196  faclbnd4lem4  14202  hashgadd  14283  hashmap  14341  hashf1lem2  14361  hashf1  14362  seqcoll  14369  cshweqrep  14715  relexpsucnnl  14921  relexpcnv  14926  relexpnndm  14932  relexpaddnn  14942  rlimsqzlem  15539  lo1le  15542  iseraltlem2  15573  fsum2d  15661  modfsummod  15684  fsumabs  15691  fsumrlim  15701  fsumo1  15702  fsumiun  15711  binom  15720  climcndslem1  15739  climcndslem2  15740  cvgrat  15773  clim2prod  15778  prodfn0  15784  prodfrec  15785  ntrivcvgfvn0  15789  fprodabs  15862  fprod2d  15869  binomfallfac  15929  bpolycl  15940  fprodefsum  15982  demoivreALT  16088  ruclem8  16124  ruclem9  16125  dvdsfac  16213  bitsinv1  16327  sadcadd  16343  sadadd2  16345  saddisjlem  16349  smuval2  16367  smupvallem  16368  smu01lem  16370  smupval  16373  smueqlem  16375  smumullem  16377  rplpwr  16443  nn0seqcvgd  16451  seq1st  16452  alginv  16456  algcvga  16460  algfx  16461  prmdvdsexp  16596  prmfac1  16602  eulerthlem2  16659  pcmpt  16769  pcfac  16776  prmpwdvds  16781  prmreclem4  16796  vdwlem10  16867  ramcl  16906  mreexexd  17533  frmdgsum  18677  mulgnnass  18916  mhmmulg  18922  gsumwrev  19152  gsmsymgrfix  19215  gsmsymgreq  19219  efginvrel2  19514  efgsrel  19521  gsum2dlem2  19753  ablfac1eulem  19856  pgpfac  19868  srgmulgass  19953  srgpcomp  19954  srgbinom  19967  lmodvsmmulgdi  20372  cnfldexp  20846  assamulgscm  21320  mplcoe1  21454  mplcoe3  21455  mplcoe5  21457  mptcoe1fsupp  21602  coe1fzgsumdlem  21688  coe1fzgsumd  21689  gsummoncoe1  21691  evl1gsumdlem  21738  evl1gsumd  21739  mdetunilem9  21985  mptcoe1matfsupp  22167  mp2pm2mplem4  22174  chpdmat  22206  tgcl  22335  fiuncmp  22771  2ndcsep  22826  1stcelcls  22828  ptcmpfi  23180  tmdgsum  23462  fsumcn  24249  caubl  24688  caublcls  24689  ovolunlem1a  24876  ovolfiniun  24881  volfiniun  24927  voliunlem1  24930  volsuplem  24935  volsup  24936  dyadmax  24978  itgfsum  25207  dvnadd  25309  cpnord  25315  dvnfre  25332  dvmptfsum  25355  ply1divex  25517  fta1g  25548  plyco  25618  dgrcolem1  25650  dgrco  25652  dvnply2  25663  plydivex  25673  aaliou3lem2  25719  dvntaylp  25746  taylthlem1  25748  cxpmul2  26060  jensen  26354  ftalem2  26439  bcmono  26641  bposlem5  26652  lgsquad2lem2  26749  dchrisumlem1  26853  dchrisum0flb  26874  pntpbnd1  26950  pntlemf  26969  qabvle  26989  qabvexp  26990  ostthlem2  26992  ostth2lem2  26998  nosupbnd1lem5  27076  noinfbnd1lem5  27091  rusgrnumwwlk  28962  eupth2lems  29224  eupth2  29225  ipasslem1  29815  mdslmd1lem1  31309  mdslmd1lem2  31310  iuninc  31525  ssrelf  31580  nn0min  31765  gsumle  31981  gsumvsca1  32110  gsumvsca2  32111  ofldchr  32156  cmppcmp  32496  nexple  32665  esumfzf  32725  sseqp1  33052  rrvsum  33111  signstfvc  33243  bnj1174  33672  lfuhgr2  33769  subfacp1lem6  33836  mrsubvrs  34173  bccolsum  34368  iprodefisumlem  34369  faclimlem1  34372  onsuct0  34959  findfvcl  34970  poimirlem28  36152  sdclem2  36247  seqpo  36252  incsequz  36253  mettrifi  36262  heiborlem4  36319  bfplem1  36327  pclfinclN  38459  uzindd  40480  nnaddcom  40827  nnadddir  40829  nnmulcom  40831  sn-sup2  40981  incssnn0  41077  mzpexpmpt  41111  pell14qrexpclnn0  41232  monotuz  41308  rmxypos  41314  jm2.17a  41327  jm2.17b  41328  rmygeid  41331  jm2.18  41355  jm2.19lem3  41358  jm2.15nn0  41370  jm2.16nn0  41371  dfac11  41432  pwslnm  41464  hbtlem5  41498  cnsrexpcl  41535  cantnfresb  41702  onmcl  41709  naddonnn  41755  relexpxpnnidm  42063  relexpiidm  42064  relexpss1d  42065  iunrelexpmin1  42068  relexpmulnn  42069  iunrelexpmin2  42072  relexp0a  42076  trclimalb2  42086  dvgrat  42680  lmodvsmdi  46544  tfis2d  47211
  Copyright terms: Public domain W3C validator