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  121  pm2.24d  154  conax1k  174  pm2.521g2  178  pm2.61iii  188  mtod  201  imbi2d  344  adantr  484  jctild  529  jctird  530  anbi2d  631  anbi1d  632  pm3.4  809  impsingle  1629  meredith  1643  stdpc4  2074  ax12  2447  ax12vALT  2494  nfsb4t  2541  nfsb4tALT  2606  moexexlem  2714  pm2.61da3ne  3103  ralrimivw  3178  reximdv  3265  rexlimdvw  3282  vtocl2d  3543  reuind  3730  reuan  3863  rexn0  4437  2reu4  4449  tppreqb  4722  ssprsseq  4742  n0snor2el  4748  prnebg  4770  prel12g  4778  elpreqprlem  4780  3elpr2eq  4823  disjord  5040  disjiund  5042  dtru  5258  propssopi  5385  opthhausdorff  5394  fr0  5521  ssrel2  5646  poltletr  5979  reuop  6131  ordsssuc2  6266  ordnbtwn  6268  ndmfv  6691  fveqres  6703  fmptco  6882  funsndifnop  6904  tpres  6954  fntpb  6963  elunirn  7002  isof1oopb  7071  fvmptopab  7202  ndmovord  7332  ordsucelsuc  7531  tfinds  7568  tfindsg  7569  limomss  7579  findsg  7604  finds1  7606  xpexr  7618  bropopvvv  7781  bropfvvvvlem  7782  bropfvvvv  7783  soxp  7819  suppun  7846  extmptsuppeq  7850  funsssuppss  7852  suppss  7856  suppssov1  7858  suppss2  7860  suppssfv  7862  suppco  7866  mpoxopynvov0  7880  smofvon2  7989  oaordi  8168  oawordeulem  8176  odi  8201  omeulem1  8204  brdomg  8515  snmapen  8586  fopwdom  8621  fodomr  8665  mapxpen  8680  infensuc  8692  onomeneq  8706  fineqvlem  8729  fineqv  8730  xpfi  8786  finsschain  8828  fsuppun  8849  fsuppunbi  8851  funsnfsupp  8854  dffi3  8892  fisup2g  8929  fisupcl  8930  fiinf2g  8961  infsupprpr  8965  wemapso2  9014  epnsym  9069  en3lplem2  9073  preleqg  9075  inf3lemd  9087  r1ordg  9204  r1val1  9212  r1pw  9271  r1pwALT  9272  rankxplim3  9307  eldju2ndl  9350  eldju2ndr  9351  carddomi2  9396  fidomtri  9419  pr2ne  9429  alephon  9493  alephcard  9494  alephnbtwn  9495  alephordi  9498  iunfictbso  9538  fin23lem30  9762  fin1a2lem10  9829  axdc3lem2  9871  axdc3lem4  9873  alephval2  9992  cfpwsdom  10004  axextnd  10011  axrepnd  10014  axpownd  10021  axregnd  10024  axinfndlem1  10025  fpwwe2lem12  10061  wunfi  10141  addnidpi  10321  pinq  10347  mulgt0sr  10525  dedekind  10801  nnind  11652  nn1m1nn  11655  nn0n0n1ge2b  11960  nn0lt2  12042  nn0le2is012  12043  uzm1  12273  uzinfi  12325  nn01to3  12338  xrltnsym  12527  xrlttri  12529  xrlttr  12530  qbtwnxr  12590  xltnegi  12606  xnn0xaddcl  12625  xlt2add  12650  xrsupsslem  12697  xrinfmsslem  12698  xrub  12702  reltxrnmnf  12732  fzospliti  13073  elfzonlteqm1  13117  elfznelfzo  13146  injresinjlem  13161  injresinj  13162  modfzo0difsn  13315  addmodlteq  13318  ssnn0fi  13357  fsuppmapnn0fiub0  13365  suppssfz  13366  seqfveq2  13397  monoord  13405  seqf1o  13416  seqhomo  13422  expnngt1  13607  faclbnd4lem4  13661  hasheqf1oi  13717  hashrabsn1  13740  hashgt0elex  13767  hash1snb  13785  hashf1lem2  13819  hashf1  13820  seqcoll  13827  hashle2pr  13840  pr2pwpr  13842  hashge2el2difr  13844  swrdnnn0nd  14018  swrdnd0  14019  pfxnd0  14050  swrdswrd  14067  pfxccatin12lem3  14094  pfxccat3  14096  swrdccat3blem  14101  repsdf2  14140  repswsymballbi  14142  cshw0  14156  cshwmodn  14157  cshwn  14159  cshwcl  14160  cshwlen  14161  cshw1  14184  2cshwcshw  14187  cshimadifsn  14191  s3sndisj  14327  s3iunsndisj  14328  relexprelg  14397  relexpnndm  14400  relexpaddg  14412  relexpaddd  14413  rexuz3  14708  rexanuz2  14709  limsupgre  14838  rlimconst  14901  caurcvg  15033  caucvg  15035  sumss  15081  fsumcl2lem  15088  modfsummods  15148  fsumrlim  15166  fsumo1  15167  fprodcl2lem  15304  dvdsaddre2b  15657  dvdsabseq  15663  mod2eq1n2dvds  15696  nno  15731  sumeven  15736  sumodd  15737  nn0seqcvgd  15912  lcmdvds  15950  lcmfunsnlem2  15982  lcmfunsnlem  15983  divgcdcoprm0  16007  ge2nprmge4  16043  exprmfct  16046  rpexp1i  16063  prm23lt5  16149  prm23ge5  16150  pcz  16215  pcadd  16223  pcmptcl  16225  oddprmdvds  16237  prmgaplem6  16390  prmgaplem7  16391  cshwshashlem1  16429  cshwsdisj  16432  prmlem0  16439  setsstruct  16523  ressress  16562  initoeu2lem2  17275  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  dfgrp2e  18129  dfgrp3e  18199  cyccom  18346  symgextf1  18549  gsmsymgrfix  18556  gsmsymgreq  18560  sylow1lem1  18723  efgsf  18855  efgrelexlema  18875  dprdss  19151  ablfac1eulem  19194  lssssr  19725  01eq0ring  20045  psrvscafval  20170  mplcoe1  20246  mplcoe5  20249  mpfrcl  20298  psgnodpm  20732  mamudm  20999  matmulcell  21054  dmatmul  21106  scmatsgrp1  21131  mavmuldm  21159  mavmulsolcl  21160  mdetunilem9  21229  cramerlem3  21298  cramer0  21299  chpscmatgsumbin  21452  chp0mat  21454  fvmptnn04ifc  21460  fvmptnn04ifd  21461  epttop  21617  neiptopnei  21740  fiuncmp  22012  1stcrest  22061  kgenss  22151  hmeofval  22366  fbun  22448  fgss2  22482  filuni  22493  filssufilg  22519  filufint  22528  hausflimi  22588  hausflim  22589  hauspwpwf1  22595  fclscmp  22638  alexsubALTlem4  22658  ptcmplem3  22662  ptcmplem5  22664  cstucnd  22893  isxmet2d  22937  imasdsf1olem  22983  blfps  23016  blf  23017  metrest  23134  nrginvrcn  23301  nmoge0  23330  nmoleub  23340  fsumcn  23478  cmetcaulem  23895  iscmet3  23900  iscmet2  23901  bcthlem2  23932  ovolicc2lem3  24126  itg2seq  24349  itg2splitlem  24355  itgeq1f  24378  itgeq2  24384  iblcnlem  24395  itgfsum  24433  limcnlp  24484  perfdvf  24509  dvnres  24537  dvmptfsum  24581  c1lip1  24603  abelth  25039  cxpsqrtth  25323  rlimcnp  25554  xrlimcnp  25557  jensen  25577  ppiublem1  25789  dchrelbas3  25825  bcmono  25864  zabsle1  25883  gausslemma2dlem0f  25948  gausslemma2dlem1a  25952  gausslemma2dlem4  25956  lgsquad2lem2  25972  2lgslem1a1  25976  2lgslem3  25991  2lgs  25994  2lgsoddprm  26003  2sqlem10  26015  2sqnn  26026  addsqnreup  26030  2sqreultblem  26035  2sqreunnltblem  26038  pntrsumbnd2  26154  pntpbnd1  26173  pntlem3  26196  axcontlem7  26767  elntg2  26782  ausgrusgrb  26961  usgredg2v  27020  lfuhgr1v0e  27047  subumgredg2  27078  upgrreslem  27097  umgrreslem  27098  fusgrfisbase  27121  nbuhgr  27136  uhgrnbgr0nb  27147  nbgr0vtxlem  27148  nbgr1vtx  27151  cusgredg  27217  cusgrsizeinds  27245  sizusglecusg  27256  finsumvtxdg2size  27343  ewlkle  27398  upgriswlk  27433  pthdivtx  27521  usgr2trlncl  27552  crctcshwlkn0lem4  27602  wwlksn  27626  iswwlksnon  27642  iswspthsnon  27645  wwlksm1edg  27670  wwlksnfi  27695  2pthdlem1  27719  umgr2wlk  27738  umgrclwwlkge2  27779  clwlkclwwlklem2a  27786  clwlkclwwlk  27790  clwlkclwwlkf1lem2  27793  clwlkclwwlkf  27796  clwwisshclwws  27803  clwwlknlbonbgr1  27827  clwwlknon0  27881  clwwlknonel  27883  clwwlknonex2e  27898  3pthdlem1  27952  eupth2  28027  nfrgr2v  28060  frgr3vlem1  28061  1to2vfriswmgr  28067  1to3vfriswmgr  28068  vdgn1frgrv2  28084  frgrncvvdeqlem9  28095  frgrwopreglem4a  28098  frgrregorufr0  28112  frgrregorufr  28113  2wspmdisj  28125  2clwwlk2clwwlklem  28134  frgrreggt1  28181  frgrreg  28182  frgrregord13  28184  aevdemo  28248  shsvs  29109  0cnop  29765  0cnfn  29766  cnlnssadj  29866  ssmd1  30097  ssmd2  30098  atexch  30167  mdsymlem4  30192  sumdmdlem  30204  rabeqsnd  30273  ifeqeqx  30308  fmptcof2  30413  padct  30466  nnindf  30546  pwsiga  31446  pwldsys  31473  ldsysgenld  31476  fiunelros  31490  breprexp  31961  bnj151  32206  bnj594  32241  bnj600  32248  subfacp1lem6  32489  erdszelem8  32502  cvmliftlem7  32595  cvmliftlem10  32598  cvmlift2lem12  32618  sat1el2xp  32683  mrsubfval  32812  msubfval  32828  mclsssvlem  32866  trpredlem1  33123  poseq  33152  nolesgn2o  33235  funpartfv  33463  endofsegid  33603  broutsideof2  33640  a1i24  33706  nn0prpwlem  33727  nn0prpw  33728  ordcmp  33852  findreccl  33858  bj-ax6e  34058  bj-ax12v3ALT  34077  bj-dtru  34198  bj-xpnzex  34339  bj-ideqg1  34524  rdgssun  34740  finxp00  34764  domalom  34766  isinf2  34767  fvineqsneq  34774  wl-spae  34871  wl-nfs1t  34887  poimirlem27  35029  ovoliunnfl  35044  voliunnfl  35046  volsupnfl  35047  itg2addnclem3  35055  itg2addnc  35056  ftc1anc  35083  areacirclem1  35090  sdclem2  35125  fdc  35128  mettrifi  35140  isexid2  35238  zerdivemp1x  35330  smprngopr  35435  mpobi123f  35545  mptbi12f  35549  ac6s6  35555  relcnveq3  35683  elrelscnveq3  35836  jca3  36097  ax12fromc15  36146  hbequid  36150  dvelimf-o  36170  ax12eq  36182  ax12el  36183  ax12indalem  36186  ax12inda2ALT  36187  ax12inda2  36188  lfl1dim  36362  lfl1dim2N  36363  lkreqN  36411  cvrexchlem  36660  ps-2  36719  paddasslem14  37074  idldil  37355  isltrn2N  37361  cdleme25a  37594  dibglbN  38407  dihlsscpre  38475  dvh4dimlem  38684  lcfl7N  38742  mapdval2N  38871  sn-dtru  39339  nn0rppwr  39420  monotoddzzfi  39799  rp-fakeimass  40136  clublem  40226  relexpnul  40295  grur1cld  40860  ee121  41131  ee122  41132  rspsbc2  41160  ax6e2ndeq  41185  vd12  41226  vd13  41227  ee221  41276  ee212  41278  ee112  41281  ee211  41284  ee210  41286  ee201  41288  ee120  41290  ee021  41292  ee012  41294  ee102  41296  ee03  41367  ee31  41378  ee31an  41380  ee123  41389  ax6e2ndeqVD  41535  ax6e2ndeqALT  41557  refsum2cnlem1  41586  fiiuncl  41619  eliin2f  41662  disjrnmpt2  41740  disjinfi  41745  rnmptbdlem  41818  allbutfi  41955  infxrunb3rnmpt  41991  infrpgernmpt  42030  monoordxrv  42047  mccl  42166  constlimc  42192  limclner  42219  xlimmnfvlem1  42400  xlimpnfvlem1  42404  ioodvbdlimc1lem2  42500  ioodvbdlimc2lem  42502  dvmptfprod  42513  dvnprodlem3  42516  stoweidlem31  42599  pwsal  42883  prsal  42886  sge0pnffigt  42961  sge0ltfirp  42965  0ome  43094  hoicvrrex  43121  hoidmvle  43165  ovnhoilem1  43166  ovnlecvr2  43175  smflimlem3  43332  funressnfv  43561  euoreqb  43591  ndmaovass  43688  afv2orxorb  43710  otiunsndisjX  43761  nltle2tri  43796  fzoopth  43810  smonoord  43814  iccpartigtl  43866  icceuelpartlem  43878  iccpartnel  43881  sprsymrelfolem2  43936  prproropf1olem4  43949  paireqne  43954  reupr  43965  reuopreuprim  43969  fmtnoprmfac1  44008  fmtnoprmfac2  44010  prmdvdsfmtnof1lem2  44028  31prm  44040  lighneallem3  44051  lighneallem4b  44053  lighneallem4  44054  lighneal  44055  nn0o1gt2ALTV  44138  nn0oALTV  44140  odd2prm2  44162  even3prm2  44163  fpprwppr  44183  stgoldbwt  44220  sbgoldbwt  44221  sbgoldbalt  44225  sbgoldbo  44231  nnsum3primesgbe  44236  wtgoldbnnsum4prm  44246  bgoldbnnsum3prm  44248  bgoldbtbndlem2  44250  bgoldbtbndlem3  44251  bgoldbtbndlem4  44252  bgoldbtbnd  44253  bgoldbachlt  44257  tgblthelfgott  44259  upgrwlkupwlk  44294  nrhmzr  44423  rngccatidALTV  44539  funcrngcsetcALT  44549  ringccatidALTV  44602  lincdifsn  44759  lindslinindimp2lem1  44793  lindsrng01  44803  ldepsnlinc  44843  m1modmmod  44861  blen1b  44928  nn0sumshdiglemB  44960  nn0sumshdiglem1  44961  reorelicc  45050  rrx2xpref1o  45058  rrx2plord2  45062  rrxlinesc  45075  line2ylem  45091  line2xlem  45093
  Copyright terms: Public domain W3C validator