MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1d Structured version   Visualization version   GIF version

Theorem a1d 25
Description: Deduction introducing an embedded antecedent. Deduction form of ax-1 6 and a1i 11. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypothesis
Ref Expression
a1d.1 (𝜑𝜓)
Assertion
Ref Expression
a1d (𝜑 → (𝜒𝜓))

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2 (𝜑𝜓)
2 ax-1 6 . 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:  2a1d  26  a1i13  27  syl5com  31  mpid  44  syld  47  imim2d  57  syl6ci  71  syl5d  73  syl6d  75  pm2.21d  118  pm2.24d  147  pm2.51  165  pm2.521  166  pm2.61iii  179  mtod  189  impbid21d  201  imbi2d  330  adantr  481  jctild  565  jctird  566  pm3.4  583  anbi2d  739  anbi1d  740  ad4ant13  1289  ad4ant134  1293  meredith  1563  ax12  2303  ax12OLD  2340  nfsb4t  2388  ax12vALT  2427  moexex  2540  pm2.61da3ne  2879  ralrimivw  2961  reximdv  3010  rexlimdvw  3027  reuind  3393  sbcimdvOLD  3481  rexn0  4046  eqoreldifOLD  4197  tppreqb  4305  ssprsseq  4325  n0snor2el  4332  prnebg  4357  elpreqprlem  4363  axsep  4740  dtru  4817  propeqop  4930  propssopi  4931  fr0  5053  ssrel2  5171  poltletr  5487  ordsssuc2  5773  ordnbtwn  5775  ndmfv  6175  fveqres  6187  fmptco  6351  funsndifnop  6370  tpres  6420  fntpb  6427  elunirn  6463  isof1oopb  6529  fvmptopab  6650  ndmovord  6777  ordsucelsuc  6969  tfinds  7006  tfindsg  7007  limomss  7017  findsg  7040  finds1  7042  xpexr  7053  bropopvvv  7200  bropfvvvvlem  7201  bropfvvvv  7202  soxp  7235  suppun  7260  extmptsuppeq  7264  funsssuppss  7266  suppss  7270  suppssov1  7272  suppss2  7274  suppssfv  7276  mpt2xopynvov0  7289  smofvon2  7398  oaordi  7571  oawordeulem  7579  odi  7604  brdomg  7909  map1  7980  fopwdom  8012  fodomr  8055  mapxpen  8070  infensuc  8082  onomeneq  8094  fineqvlem  8118  fineqv  8119  xpfi  8175  finsschain  8217  fsuppun  8238  fsuppunbi  8240  funsnfsupp  8243  dffi3  8281  fisup2g  8318  fisupcl  8319  fiinf2g  8350  wemapso2  8402  en3lplem2  8456  inf3lemd  8468  r1ordg  8585  r1val1  8593  r1pw  8652  r1pwALT  8653  rankxplim3  8688  carddomi2  8740  fidomtri  8763  pr2ne  8772  alephon  8836  alephcard  8837  alephnbtwn  8838  alephordi  8841  iunfictbso  8881  fin23lem30  9108  fin1a2lem10  9175  axdc3lem2  9217  axdc3lem4  9219  alephval2  9338  cfpwsdom  9350  axextnd  9357  axrepnd  9360  axpownd  9367  axregnd  9370  axinfndlem1  9371  fpwwe2lem12  9407  wunfi  9487  addnidpi  9667  pinq  9693  mulgt0sr  9870  dedekind  10144  nnind  10982  nn1m1nn  10984  nn0n0n1ge2b  11303  nn0lt2  11384  nn0le2is012  11385  uzm1  11662  uzinfi  11712  nn01to3  11725  xrltnsym  11914  xrlttri  11916  xrlttr  11917  qbtwnxr  11974  xltnegi  11990  xnn0xaddcl  12009  xlt2add  12033  xrsupsslem  12080  xrinfmsslem  12081  xrub  12085  reltxrnmnf  12114  fzospliti  12441  elfzonlteqm1  12484  elfznelfzo  12514  injresinjlem  12528  injresinj  12529  modfzo0difsn  12682  addmodlteq  12685  ssnn0fi  12724  fsuppmapnn0fiub0  12733  suppssfz  12734  seqfveq2  12763  seqshft2  12767  monoord  12771  seqsplit  12774  seqf1o  12782  seqhomo  12788  faclbnd4lem4  13023  hasheqf1oi  13080  hasheqf1oiOLD  13081  hashrabsn1  13103  hashgt0elex  13129  hash1snb  13147  hashf1lem2  13178  hashf1  13179  seqcoll  13186  hashle2pr  13197  pr2pwpr  13199  hashge2el2difr  13201  2swrd1eqwrdeq  13392  swrdswrd  13398  swrdccatin1  13420  swrdccatin12lem3  13427  swrdccat3  13429  swrdccat3blem  13432  repsdf2  13462  repswsymballbi  13464  cshw0  13477  cshwmodn  13478  cshwn  13480  cshwcl  13481  cshwlen  13482  cshw1  13505  2cshwcshw  13508  cshimadifsn  13512  s3sndisj  13640  s3iunsndisj  13641  relexprelg  13712  relexpnndm  13715  relexpaddg  13727  relexpaddd  13728  resqrex  13925  rexuz3  14022  rexanuz2  14023  limsupgre  14146  rlimconst  14209  caurcvg  14341  caucvg  14343  sumss  14388  fsumcl2lem  14395  modfsummods  14452  fsumrlim  14470  fsumo1  14471  fprodcl2lem  14605  dvdsaddre2b  14953  dvdsabseq  14959  mod2eq1n2dvds  14995  nno  15022  sumeven  15034  sumodd  15035  nn0seqcvgd  15207  lcmdvds  15245  lcmfunsnlem2  15277  lcmfunsnlem  15278  divgcdcoprm0  15303  exprmfct  15340  rpexp1i  15357  prm23lt5  15443  prm23ge5  15444  pcz  15509  pcadd  15517  pcmptcl  15519  oddprmdvds  15531  prmgaplem5  15683  prmgaplem6  15684  prmgaplem7  15685  cshwshashlem1  15726  cshwsdisj  15729  prmlem0  15736  setsstruct  15819  ressress  15859  initoeu2lem2  16586  mgm2nsgrplem2  17327  mgm2nsgrplem3  17328  dfgrp2e  17369  dfgrp3e  17436  symgextf1  17762  gsmsymgrfix  17769  gsmsymgreq  17773  sylow1lem1  17934  efgsf  18063  efgrelexlema  18083  dprdss  18349  ablfac1eulem  18392  lssssr  18872  01eq0ring  19191  psrvscafval  19309  mplcoe1  19384  mplcoe5  19387  mpfrcl  19437  psgnodpm  19853  mamudm  20113  matmulcell  20170  dmatmul  20222  scmatsgrp1  20247  mavmuldm  20275  mavmulsolcl  20276  mdetunilem9  20345  cramerlem3  20414  cramer0  20415  chpscmatgsumbin  20568  chp0mat  20570  fvmptnn04ifc  20576  fvmptnn04ifd  20577  epttop  20723  neiptopnei  20846  fiuncmp  21117  1stcrest  21166  comppfsc  21245  kgenss  21256  hmeofval  21471  fbun  21554  fgss2  21588  filuni  21599  filssufilg  21625  filufint  21634  hausflimi  21694  hausflim  21695  hauspwpwf1  21701  fclscmp  21744  alexsubALTlem4  21764  ptcmplem3  21768  ptcmplem5  21770  cstucnd  21998  isxmet2d  22042  imasdsf1olem  22088  blfps  22121  blf  22122  metrest  22239  nrginvrcn  22406  nmoge0  22435  nmoleub  22445  fsumcn  22581  cmetcaulem  22994  iscmet3  22999  iscmet2  23000  bcthlem2  23030  ovolicc2lem3  23194  itg2seq  23415  itg2splitlem  23421  itgeq1f  23444  itgeq2  23450  iblcnlem  23461  itgfsum  23499  limcnlp  23548  perfdvf  23573  dvnres  23600  dvmptfsum  23642  c1lip1  23664  abelth  24099  sinq12ge0  24164  rlimcnp  24592  xrlimcnp  24595  jensen  24615  ppiublem1  24827  dchrelbas3  24863  bcmono  24902  zabsle1  24921  gausslemma2dlem0f  24986  gausslemma2dlem1a  24990  gausslemma2dlem4  24994  lgsquad2lem2  25010  2lgslem1a1  25014  2lgslem3  25029  2lgs  25032  2lgsoddprm  25041  2sqlem10  25053  pntrsumbnd2  25156  pntpbnd1  25175  pntlem3  25198  axcontlem7  25750  ausgrusgrb  25953  usgredg2v  26012  lfuhgr1v0e  26039  subumgredg2  26070  fusgrfisbase  26108  nbuhgr  26126  uhgrnbgr0nb  26137  nbgr0vtxlem  26138  nbgr1vtx  26141  uvtxa0  26181  uvtx2vtx1edg  26186  cusgredg  26207  cusgrsizeinds  26235  sizusglecusg  26246  ewlkle  26371  upgriswlk  26406  pthdivtx  26494  usgr2trlncl  26525  crctcshwlkn0lem4  26574  wwlksn  26598  iswwlksnon  26609  iswspthsnon  26610  wwlksm1edg  26636  wwlksnfi  26670  wwlksnonfi  26685  wspn0  26689  2pthdlem1  26695  umgr2wlk  26714  2wspdisj  26723  2wspiundisj  26724  clwwlksn  26748  clwlkclwwlklem2a  26766  clwlkclwwlk  26770  umgrclwwlksge2  26778  clwwlksnfi  26779  clwwisshclwws  26794  clwwnisshclwwsn  26796  3pthdlem1  26890  eupth2  26965  nfrgr2v  27000  frgr3vlem1  27001  1to2vfriswmgr  27007  1to3vfriswmgr  27008  vdgn1frgrv2  27024  frgrwopreglem3  27041  frgrwopreglem4  27042  frgrwopreg  27044  frgrregorufr0  27047  frgrregorufr  27048  fusgr2wsp2nb  27056  2wspmdisj  27059  numclwwlkovf2ex  27075  extwwlkfab  27078  frgrreggt1  27105  frgrreg  27106  frgrregord13  27108  aevdemo  27171  shsvs  28031  0cnop  28687  0cnfn  28688  cnlnssadj  28788  ssmd1  29019  ssmd2  29020  atexch  29089  mdsymlem4  29114  sumdmdlem  29126  ifeqeqx  29208  fmptcof2  29299  padct  29340  nnindf  29406  pwsiga  29974  ldsysgenld  30004  fiunelros  30018  bnj151  30655  bnj594  30690  bnj600  30697  subfacp1lem6  30875  erdszelem8  30888  cvmliftlem7  30981  cvmliftlem10  30984  cvmlift2lem12  31004  mrsubfval  31113  msubfval  31129  mclsssvlem  31167  trpredlem1  31428  poseq  31451  funpartfv  31694  endofsegid  31834  broutsideof2  31871  a1i24  31937  nn0prpwlem  31959  nn0prpw  31960  ordcmp  32088  findreccl  32094  bj-alsb  32267  bj-ax6e  32295  bj-ax12v3ALT  32318  bj-axsep  32436  bj-dtru  32440  bj-xpnzex  32593  bj-xnex  32701  finxp00  32871  wl-spae  32938  wl-nfs1t  32956  poimirlem27  33068  ovoliunnfl  33083  voliunnfl  33085  volsupnfl  33086  itg2addnclem3  33095  itg2addnc  33096  ftc1anc  33125  areacirclem1  33132  sdclem2  33170  fdc  33173  mettrifi  33185  isexid2  33286  zerdivemp1x  33378  smprngopr  33483  mpt2bi123f  33603  mptbi12f  33607  ac6s6  33612  jca3  33618  ax12fromc15  33670  hbequid  33674  dvelimf-o  33694  ax12eq  33706  ax12el  33707  ax12indalem  33710  ax12inda2ALT  33711  ax12inda2  33712  lfl1dim  33888  lfl1dim2N  33889  lkreqN  33937  cvrexchlem  34185  ps-2  34244  paddasslem14  34599  idldil  34880  isltrn2N  34886  cdleme25a  35121  dibglbN  35935  dihlsscpre  36003  dvh4dimlem  36212  lcfl7N  36270  mapdval2N  36399  monotoddzzfi  36987  rp-fakeimass  37338  clublem  37398  relexpnul  37451  ee121  38193  ee122  38194  rspsbc2  38226  ax6e2ndeq  38257  vd12  38307  vd13  38308  ee221  38357  ee212  38359  ee112  38362  ee211  38365  ee210  38367  ee201  38369  ee120  38371  ee021  38373  ee012  38375  ee102  38377  ee03  38450  ee31  38461  ee31an  38463  ee123  38472  ax6e2ndeqVD  38628  ax6e2ndeqALT  38650  refsum2cnlem1  38679  fiiuncl  38719  eliin2f  38772  disjrnmpt2  38849  disjinfi  38854  rnmptbd2lem  38939  rnmptbdlem  38946  allbutfi  39080  infxrunb3rnmpt  39119  mccl  39234  constlimc  39260  limclner  39287  ioodvbdlimc1lem2  39453  ioodvbdlimc2lem  39455  dvmptfprod  39466  dvnprodlem3  39469  stoweidlem31  39555  pwsal  39842  prsal  39845  sge0pnffigt  39920  sge0ltfirp  39924  0ome  40050  hoicvrrex  40077  hoidmvle  40121  ovnhoilem1  40122  ovnlecvr2  40131  smflimlem3  40288  reuan  40484  2reu4  40494  funressnfv  40512  ndmaovass  40590  otiunsndisjX  40595  nltle2tri  40620  fzoopth  40634  smonoord  40639  iccpartigtl  40657  icceuelpartlem  40669  iccpartnel  40672  pfxccat3  40725  fmtnoprmfac1  40776  fmtnoprmfac2  40778  prmdvdsfmtnof1lem2  40796  31prm  40811  lighneallem3  40823  lighneallem4b  40825  lighneallem4  40826  lighneal  40827  nn0o1gt2ALTV  40904  nn0oALTV  40906  stgoldbwt  40959  bgoldbwt  40960  sgoldbalt  40964  nnsum3primesgbe  40969  wtgoldbnnsum4prm  40979  bgoldbnnsum3prm  40981  bgoldbtbndlem2  40983  bgoldbtbndlem3  40984  bgoldbtbndlem4  40985  bgoldbtbnd  40986  bgoldbachlt  40988  tgblthelfgott  40990  bgoldbachltOLD  40995  tgblthelfgottOLD  40997  upgrwlkupwlk  41009  sprsymrelfolem2  41031  nrhmzr  41161  rngccatidALTV  41277  funcrngcsetcALT  41287  ringccatidALTV  41340  lincdifsn  41501  lindslinindimp2lem1  41535  lindsrng01  41545  ldepsnlinc  41585  m1modmmod  41604  blen1b  41674  nn0sumshdiglemB  41706  nn0sumshdiglem1  41707
  Copyright terms: Public domain W3C validator