Theorem ancoms 482

Description: Inference commuting conjunction in antecedent. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 12) -type inference in a proof.

Hypothesis

Ref	Expression
ancoms.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
ancoms	|- ((ps /\ ph) -> ch)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancom 480	. 2 |- ((ps /\ ph) <-> (ph /\ ps))
2		ancoms.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	sylbi 215	1 |- ((ps /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ wa 239

This theorem is referenced by:  anabsi8 553  anabss4 556  sylan9bbr 597  bi2anan9r 692  pm5.18 719  mpancom 766  3adantr1 914  3adantr2 915  3adantr3 916  syl3anr1 996  syl3anr2 997  syl3anr3 998  mp3anr1 1035  mp3anr2 1036  mp3anr3 1037  2exeu 1687  2eu1 1690  2eu3 1692  eqeqan12rd 1740  sylan9eqr 1788  rcla4cvaOLD 2213  sbccomglem 2358  sbccomg 2359  csbcomg 2393  csbnestg 2414  sbcnestg 2416  sylan9ssr 2463  breqan12rd 3175  ordelssne 3500  ordtri3or 3506  ordtri3orOLD 3507  ordtri2 3511  ordtri4 3514  ordtr2 3523  ordtri2or 3577  ordtri2orOLD 3578  difex2OLD 3614  euobj1 3645  dfwe2 3672  ordsucelsuc 3713  ordunisuc2 3737  tfindsg 3755  tfindsg2 3756  dfom2 3762  ordomOLD 3772  findsg 3791  weinxp 3870  brelrng 4001  dminss 4141  imainss 4142  dfco2a 4205  coexg 4240  funeq 4252  funeuOLD 4256  funco 4268  funcoOLD 4269  funcnvuni 4293  cofunex2g 4313  f1co 4423  dff1o2OLD 4451  f1ocnv 4462  f1ocnvOLD 4463  resdif 4470  funimass4 4533  fvelima 4534  dffv2 4545  fsn2 4620  isotr 4685  isotrALT 4686  opreqan12rd 4714  onopriun 4929  tfr3 4945  tz7.48-2 4977  tz7.49 4979  omclOLD 5028  oaordi 5038  oaword 5041  oawordOLD 5042  oaord1 5044  oaword2 5046  oa00 5052  oalimcl 5053  oaass 5054  oarec 5055  omord2 5057  omcan 5059  omword 5060  omword1 5063  omword2 5064  omlimcl 5068  odi 5069  omass 5070  oneo 5071  oen0 5072  oeord 5074  oecan 5075  oeword 5076  oeworde 5079  oelim2 5081  nnarcl 5098  nnaordr 5102  nnmsucr 5106  nnmsucrOLD 5107  nnmcom 5108  nnmcomOLD 5109  oaabslem 5119  oaabs 5120  omsmo 5125  ersym 5141  ecopoprsym 5180  ecoprcom 5189  mapvalg 5200  pmvalg 5201  f1oeng 5265  ener 5280  domtr 5285  fundmen 5298  xpdom2 5312  ac6sfilem3 5319  domtriord 5357  onomeneq 5422  nndomo 5424  isfinite1 5434  pssnn 5438  xpfi 5442  infcntss 5456  fiint 5460  fodomfi 5466  supmaxlem 5488  suppr 5490  ordtypelem5 5498  hartog 5503  suc11reg 5520  inf3lem5 5532  infeq5 5536  omsubsuc2 5674  omsubsdom 5677  omsubdom 5678  omsubss 5680  omsubdmss 5682  omsubindss 5684  infenomsub 5685  omsubinit 5686  aceq3 5691  aceq5 5698  zorn2lem6 5751  brdom3 5759  brdom7disj 5762  brdom6disj 5763  domtri 5785  sucdom 5790  unxpdom2 5793  sdomel 5795  alephord3 5822  aleph11 5823  cardaleph 5829  alephval2 5846  ltsopi 5964  mulclpi 5969  addcompi 5970  mulcompi 5972  ltapi 5978  ltmpi 5979  ordpipq 6004  ltrpq 6033  prnmadd 6048  genpnnp 6056  addcompr 6071  mulcompr 6073  ltsopr 6084  prlem934b 6086  prlem934 6087  ltexprlem2 6091  suplem1pr 6109  suplem2pr 6110  ltsrpr 6134  ssgt0sr 6165  axmulopr 6214  axmulass 6227  axdistr 6228  pre-axltadd 6238  cnegexlem3 6297  pncan3 6330  pncan2 6354  muladd 6378  muladdOLD 6379  subdi 6386  mulneg2 6412  negsubdi2 6419  mulsub 6440  ltxrlt 6465  xrltnle 6467  axlttri 6468  axsup 6472  ltnle 6476  letri3 6483  leloe 6484  eqlelt 6485  xrltnsym 6521  xrlttri 6523  xrleloe 6528  xrletri 6532  letric 6598  letricOLD 6599  ltleadd 6625  ltsubpos 6637  posdif 6639  addge01 6657  suble0 6660  rec11r 6751  divadddiv 6756  divdivdiv 6757  prodgt02 6800  prodge02 6802  lemul12aOLD 6820  mulgt1 6822  ltdivmul 6844  ledivmul 6846  lt2mul2div 6849  lereci 6858  le2msqi 6860  msq11i 6861  ltdiv23 6870  lediv23 6871  lediv2a 6875  xrmaxlt 6891  maxle 6896  maxlt 6900  nnmulcl 6919  nndivtr 6939  lbreu 7049  infm3 7058  dfinfmr 7071  infmsup 7072  xrsupsslem 7080  xrinfmsslem 7081  supxr 7085  supxrunb1 7093  supxrunb2 7094  supxrbnd1 7099  nn0nnaddcl 7130  nn0sub 7165  zaddcl 7169  zrevaddcl 7174  znnsub 7181  znn0sub 7182  zltp1le 7185  z2ge 7195  zextlt 7197  gtndiv 7200  prime 7202  uzwo4OLD 7217  uzwo5OLD 7218  zmax 7228  zbtwnre 7229  rebtwnz 7230  qrevaddcl 7250  qbtwnre 7254  flge 7267  fllt 7268  flwordi 7272  flval3 7274  flbi 7275  flbi2 7276  flzadd 7280  modcyc2 7312  ioon0 7331  iooin 7334  eliooord 7351  elioc2 7353  elico2 7354  elicc2 7355  iooshf 7359  iccsupr 7362  iooneg 7370  iccneg 7371  uz11 7396  uzaddcl 7413  uzwo 7419  uzwoOLD 7420  fzen 7459  elfz2nn0 7462  fzopth 7469  fzss2 7471  fzsuc 7473  fzssp1 7474  fzrev 7484  fsequb 7497  fseqsupubi 7500  om2uzlt2i 7505  om2uzf1oi 7507  seq1rn2 7529  shftval4 7557  shftval5 7558  2shfti 7560  shftcan2 7561  seqzp1 7586  seqzval2 7591  seqzrn2 7594  ser0cl1i 7602  expcllem 7613  expsub 7636  expsubOLD 7637  expordi 7640  sqr2irr 7774  mulre 7822  abslti 7922  abslei 7923  abssubne0 7929  abs3dif 7946  abs2difabs 7950  seq1bndi 7957  seq1ublem 7958  cvg2i 7969  cvganz 7971  caubndi 7973  faclbnd 7992  faclbnd5 8000  facavg 8002  bccmpl 8009  bccl2 8018  fsum1i 8060  fsum1ps 8073  fsumsplit 8075  fsumshft 8086  fsumshftm 8087  fsumconst 8093  clm3i 8134  clm4lei 8136  climfnn 8147  2climnn 8157  2climnn0 8158  climge0 8167  climaddlem3 8171  climmullem1 8175  climmullem8 8182  climsubc2 8186  clim2serz 8189  climsqueeze 8195  climsqueeze2 8196  clim2serzi 8200  climserzlei 8202  caucvglem2 8213  caucvglem6 8217  caucvgi 8218  serzf0i 8224  ser1cmp2lem 8231  ser1cmp2i 8232  dfisum 8247  infcvglem1 8277  cvgratlem2ALT 8305  cvgratlem1 8307  cvgratlem2 8308  fsum0diag4 8318  mulc1cncf 8336  ivthlem7 8344  reeftlcl 8437  demoivre 8547  demoivreALT 8548  acdc2 8554  acdc5 8557  nn0ennn 8561  infpnlem1 8570  ruclem13 8586  infxpidmlem8 8623  infunabs 8629  infcdaabs 8630  infdif 8632  infxpabs 8634  iunctb 8639  infmap2lem2 8644  eltg 8683  eltg2 8684  tgval3 8690  basgen2 8704  subtop 8711  retopbas 8720  iscld 8740  opnneiss 8803  islp2 8818  iscn 8829  iscnp 8831  cnco 8840  ismsg 8872  metreslem 8894  ssbl 8927  metequiv 8953  metcnp 8960  metcnp2 8961  ioo2bl 8985  tgioolem 8987  dscmet 8991  lmbr 9001  lmnn 9008  lmss 9026  lmclim 9036  metelcls 9038  metcnp4 9043  xplm 9048  iscms2lem4 9065  bcthlem1 9072  bcthlem17 9088  bcthlem18 9089  bcthlem19 9090  bcthlem20 9091  bcthlem21 9092  bcthlem24 9095  bcthlem25 9096  isgrp2i 9155  grplactfval 9199  ablmul 9234  ghgrpilem2 9237  ghgrpilem3 9238  ghgrpi 9240  isgalem 9244  isga 9245  ssga 9250  isring 9260  ringideu 9265  ringsn 9285  vcz 9316  isvc 9327  isnv 9358  isnvi 9359  vacnlem3 9464  sqcn 9469  va1cnlem 9479  ip1cnilem2 9508  ip1cnilem3 9509  ip1cnilem5 9511  nvo00 9558  nmoge0 9564  nmorepnf 9565  nmblolbii 9594  ipblnfi 9652  ubthlem3 9669  ubthlem4 9670  ubthlem5 9671  ubthlem11 9677  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  htthlem5 9766  htthlem6 9767  pslem 9785  spwval2 9791  spweu 9795  pilem2 9816  efif1lem7 9885  logeftb 9913  relogexp 9923  uptx 10018  txcn 10019  txcnopab 10020  hmeobc 10031  cnvhmpha 10032  elsubsp 10040  subcld 10046  subtopmetlem 10047  oefil2 10067  infi 10072  fgbas 10078  fgfil 10082  extbas1 10083  filrn 10085  limfil 10089  cncomp 10123  isdivrng 10209  hvpncan2 10333  hvaddsub4 10370  hire 10385  abshicom 10392  hial2eq2 10398  orthcom 10399  normpyc 10438  hcau2 10480  hhcms 10497  hlimcauii 10531  hhssabli 10557  hhsscms 10575  ocsh 10581  occon2 10586  chocunii 10597  projlem2 10612  projlem26 10636  pjval 10664  shscli 10706  shscom 10708  shsel2 10711  spanss 10743  shjcom 10755  shlej1 10780  shmodsi 10787  chpsscon3 10851  spansnmul 10912  spansncol 10916  pjspansn 10925  spanunsni 10927  cmcm2 10984  cm2j 10988  spansncvi 11024  5oalem2 11027  3oalem2 11035  honegsubdi2 11166  adjsym 11188  cnvadj 11245  nmopub2tALT 11262  nmfnleub2 11279  brafn 11300  kbmul 11308  kbpj 11309  nmcopexlem6 11385  lnopconi 11392  nmcfnexlem6 11414  lnfnconi 11419  riesz3i 11424  cnlnadjlem2 11430  cnlnadjlem9 11437  cnlnssadj 11442  nmopcoi 11457  cnvbraval 11473  kbass2 11480  kbass5 11483  leop 11486  leop3 11488  leopmul2i 11498  leoptri 11499  hmopidmchi 11515  pjimai 11540  cvcon3 11648  cvnsym 11654  mdbr2 11660  dmdmd 11664  dmdbr2 11667  dmdbr3 11669  dmdbr4 11670  dmdbr5 11672  mdsl0 11674  ssmd2 11676  ssdmd1 11677  ssdmd2 11678  mdslmd1lem1 11689  mdslmd1lem2 11690  mdslmd3i 11696  mdslmd4i 11697  atcveq0 11712  superpos 11718  atnem0 11741  atssma 11742  atexch 11745  atomli 11746  atcvatlem 11749  atcvati 11750  irredlem1 11754  irredlem3 11756  irredi 11758  atcvat3i 11760  atdmd 11762  mdsymlem1 11767  mdsymlem3 11769  mdsymlem4 11770  mdsymlem5 11771  mdsymlem8 11774  dmdsym 11777  atdmd2 11778  sumdmdlem 11782  cdjreui 11796  cdj3lem2b 11801  cdj3i 11805  bnj232 11867  bnj50 12216  bnj623 12432  bnj625 12433  bnj626 12434  bnj834 12500  bnj1074 12695  bnj1242 12803  bnj934 13126  bnj953 13135  bnj1498 13354  elfzp1b 13397  elfzm1b 13398  fseq1cl 13411  lediv2aALT 13413  nn0seqcvgd 13451  eluznn0 13453  negdvdsb 13463  dvdsnegb 13464  0dvds 13467  dvdsmul1 13468  muldvds1 13470  muldvds2 13471  dvdscmulr 13474  dvdssubr 13483  divalglem8 13495  divalglem9 13496  ndvdssub 13502  ndvdsadd 13503  gcdcllem1 13510  gcdcom 13518  neggcd 13525  gcdabs 13529  modgcd 13530  algrf 13531  algcvgblem 13537  mulgcdlem7 13554  coprmdvds 13575  funpsstri 13628  predep 13694  predepOLD 13695  soxp 13742  soseq 13747  wfr3g 13748  wfrlem10 13758  axsltsolem1 13796  axdenselem4 13812  axfelem1 13821  nndivsub 13988  nndivlub 13989  fiiu 14072  ficli 14081  domintref 14091  letri31 14111  mappow 14143  celsor 14173  injsurinj 14214  iscst4 14248  ubpar 14325  ranncnt 14349  dutos1 14350  lteqtpos 14352  fprod1i 14397  clfsebs 14430  fnopabco2b 14457  curgrpact 14458  nelioo5 14579  cmphmp 14598  cnvhmphb 14600  hmphsyma 14602  hmphsym 14603  hmeogrp 14612  homindlem3 14620  cnfilca 14641  conttnf 14658  trhom 14697  altretop 14707  msr4 14714  mslb1 14717  iintlem1 14720  trdom 14723  cnvtr 14726  lvsovso 14734  1ded 14767  dualded 14814  isfuna 14864  elincin 14902  tarax3a 14904  tarax3c 14906  tarax3d3 14908  cptarc 14924  tartarmap 14947  fnctartar3 14968  dmsdtriordOLD 15042  elicc3 15044  ccid 15045  fiss 15050  ordtypelem5OLD 15061  hartogOLD 15066  omsubsuc2OLD 15069  omsubsdomOLD 15072  omsubdomOLD 15073  omsubssOLD 15075  omsubdmssOLD 15077  omsubindssOLD 15079  infenomsubOLD 15080  omsubinitOLD 15081  subsubtop 15105  subcls 15106  subntr 15107  compcov 15111  compsublem 15112  compsub 15113  compfipin0lem 15117  connsub 15125  reconnlem5 15132  reconn 15133  isfne 15162  isfne3 15164  neibastop2lem3 15203  neibastop2lem4 15204  topjoin 15209  fnejoin1 15212  filfinnfr 15243  ufinffr 15260  ufilen 15261  flimcls 15270  fmfnfm 15280  fclusff 15305  sfclusf 15306  istail 15316  filnetlem1 15322  filnetlem3 15324  filnetlem4 15325  filnetlem5 15326  morex 15344  unirep 15346  opelopab3 15370  enf1f1o 15402  mapfi 15409  upixp 15411  indexa 15435  indexfi 15437  fipreima 15438  infmrgelb 15448  fimaxre 15456  filbcmb 15458  addsubeq4 15460  fzadd2 15473  fzsplit 15474  fzdisj 15475  fzm1 15478  sdclem1 15491  sdclem2 15492  sdc 15493  incsequz2 15498  csbrni 15514  subspopn 15519  subspabs 15522  lpss2 15524  metf1o 15525  mettrifi2 15530  geomcau 15531  iccsplit 15536  lincmb01cmp 15560  lincmb01icc 15561  oprpiece1res2 15563  addccncf 15565  sub1cncf 15567  sub2cncf 15568  cnimass 15570  cnres 15571  cnresima 15573  cnss 15574  haustlmu 15588  lmtlm 15590  txsubsp 15594  txmet 15607  sstotbnd 15618  totbndss 15619  isbnd3 15623  bndss 15624  totbndbnd 15626  ismtycnv 15631  ismtyhmeolem 15632  ismtybnd 15635  ismtyres 15636  heiborlem1 15637  heiborlem16 15652  heiborlem18 15654  heiborlem23 15659  heiborlem28 15664  bfplem8 15687  bfp 15691  rrndstprj1 15699  rrndstprj2 15700  rrncms 15701  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704  iccbnd 15708  exidreslem 15712  exidresid 15714  ghomco 15722  phtpycom 15732  reparphtlem2 15746  pcohtpylem2 15763  pcohtpylem3 15764  pcohtpy 15765  pcorevlem 15768  isdivrng2 15793  rngisocnv 15817  riscer 15824  crnghomfo 15836  unichnidl 15861  maxidlmax 15873  igenmin 15894  ersym2 15938  prtlem18 15961  prter1 15964  2sbc6g 16061  2sbc5g 16062  ordpss 16110  ordintdif 16122  smores2 16129  smoel 16133  strdif 16478  ringideuNEW 16875

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163  df-an 241

Copyright terms: Public domain