Theorem ancoms 436

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 10) -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 435	. 2 |- ((ps /\ ph) <-> (ph /\ ps))
2		ancoms.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	sylbi 199	1 |- ((ps /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anabsi8 497  anabss4 500  sylan9bbr 539  bi2anan9r 631  mpancom 702  3adantr1 803  3adantr2 804  3adantr3 805  syl3anr1 873  syl3anr2 874  syl3anr3 875  mp3anr1 909  mp3anr2 910  mp3anr3 911  2exeu 1423  2eu1 1426  2eu3 1428  eqeqan12rd 1467  sylan9eqr 1505  rcla4cva 1849  sbccomglem 1959  sbccomg 1960  csbcomg 1988  csbnestg 2007  sbcnestg 2009  sylan9ssr 2047  breqan12rd 2601  difex2 2840  ordelssne 2937  ordtri3or 2942  ordtri2 2945  ordtri2or 3040  ordunisuc2 3078  dfom2 3096  ordom 3104  findsg 3120  tfindsg 3125  tfindsg2 3126  weinxp 3195  dminss 3411  imainss 3412  coexg 3465  funeq 3476  funeu 3478  funco 3490  funcnvuni 3504  cofunex2g 3521  f1co 3606  f1o2 3632  f1ocnv 3640  funimass4 3702  fsn2 3775  isotr 3836  isotrALT 3837  tfr3 3865  tz7.48-2 3896  tz7.49 3898  opreqan12rd 3919  omcl 4109  oaordi 4118  oaword 4121  oaord1 4123  oaword2 4125  oa00 4131  oalimcl 4132  oaass 4133  oarec 4134  omord2 4136  omcan 4138  omword 4139  omword1 4142  omword2 4143  omlimcl 4147  odi 4148  omass 4149  oneo 4150  oen0 4151  oeord 4153  oecan 4154  oeword 4155  oeworde 4158  oelim2 4160  nnarcl 4170  nnaordr 4174  nnmsucr 4178  nnmcom 4179  oaabslem 4189  oaabs 4190  omsmo 4195  ersym 4210  ecopoprsym 4248  ecoprcom 4257  mapvalg 4268  pmvalg 4269  f1oeng 4330  ener 4345  domtr 4350  fundmen 4363  xpdom2 4376  onomeneq 4450  nndomo 4452  isfinite1 4462  pssnn 4465  infcntss 4482  fiint 4486  fodomfi 4492  suppr 4514  suc11reg 4529  inf3lem5 4541  infeq5 4545  aceq3 4657  aceq5 4664  zorn2lem6 4717  brdom3 4725  brdom7disj 4728  brdom6disj 4729  domtri 4761  sucdom 4765  unxpdom2 4768  sdomel 4770  alephord3 4801  aleph11 4802  cardaleph 4808  alephval2 4825  ltsopi 4939  mulclpi 4944  addcompi 4945  mulcompi 4947  ltapi 4953  ltmpi 4954  ordpipq 4979  ltrpq 5008  prnmadd 5023  genpnnp 5031  addcompr 5046  mulcompr 5048  ltsopr 5059  prlem934b 5061  prlem934 5062  ltexprlem2 5066  suplem1pr 5084  suplem2pr 5085  ltsrpr 5109  ssgt0sr 5140  axmulopr 5189  axmulass 5201  axdistr 5202  pre-axltadd 5212  cnegextlem3 5270  pncan3t 5300  pncan2t 5321  muladdt 5344  subdit 5350  mulneg2t 5375  negsubdi2t 5381  mulsubt 5400  ltxrltt 5423  xrltnlet 5425  axlttri 5426  axsup 5430  ltnlet 5434  letri3t 5441  leloet 5442  eqleltt 5443  xrltnsymt 5474  xrlttrit 5476  xrleloet 5481  xrletrit 5485  letrit 5545  ltleaddt 5570  posdift 5578  addge01t 5596  suble0t 5599  divcan5t 5688  divdivdivt 5692  prodgt02t 5734  prodge02t 5736  lemul12itOLD 5750  mulgt1t 5752  lerec 5779  le2msq 5781  msq11 5782  ltdiv23t 5791  lediv23t 5792  lediv2it 5796  xrmaxltt 5812  maxlet 5817  maxltt 5821  nnmulclt 5840  nndivtrt 5858  lbreu 5943  infm3 5952  dfinfmr 5965  infmsup 5966  xrsupsslem 5974  xrinfmsslem 5975  supxr 5979  supxrunb1 5987  supxrunb2 5988  supxrbnd1 5993  nn0nnaddclt 6024  nn0subt 6059  zaddclt 6063  zrevaddclt 6068  znnsubt 6075  znn0subt 6076  zltp1let 6079  z2get 6086  zextltt 6088  gtndivt 6091  primet 6093  uzwo4OLD 6109  uzwo5OLD 6110  zmax 6119  zbtwnre 6120  rebtwnz 6121  flget 6129  flltt 6130  flval3t 6133  flwordit 6134  flbit 6135  qrevaddclt 6164  qbtwnre 6167  om2uzlt2 6187  om2uzf1o 6189  seq1rn2 6209  shftval4t 6237  shftval5t 6238  2shft 6240  shftcan2t 6241  ioon0t 6257  iooint 6260  elioc2t 6273  elico2t 6274  elicc2t 6275  ioossicc 6281  iccsupr 6282  ioonegt 6290  iccnegt 6291  uz11t 6315  uzaddclt 6332  uzwo 6338  uzwoOLD 6339  elfz2nn0t 6378  fzoptht 6385  fzss2t 6387  fzssp1t 6389  fzrevt 6394  fsequb 6406  fseqsupub 6409  seqzp1 6431  seqzval2t 6436  seqzrn2 6439  ser0cl1 6447  expcllem 6458  expsubt 6480  expordit 6482  nn0opth 6547  sqr2irr 6610  abslt 6761  absle 6762  abssubne0t 6771  abs3dift 6787  abs2difabst 6791  seq1bnd 6798  seq1ublem 6799  cvg2 6810  cvganz 6812  caubnd 6814  faclbnd 6833  faclbnd5 6841  facavgt 6843  bccmplt 6851  bccl2t 6860  fsum1 6894  fsum1ps 6907  fsumsplit 6909  fsumshft 6920  fsumshftm 6921  fsumconst 6927  clm3 6968  clm4le 6970  climfnn 6981  2climnn 6990  2climnn0 6991  climge0 7000  climaddlem3 7003  climmullem1 7007  climmullem8 7014  climsubc2 7018  clim2serzt 7021  climsqueeze 7027  climsqueeze2 7028  clim2serz 7032  climserzle 7034  caucvglem2 7045  caucvglem6 7049  caucvg 7050  serzf0 7056  ser1f0 7057  ser1cmp2lem 7063  ser1cmp2 7064  dfisum 7078  infcvglem1 7107  cvgratlem2ALT 7134  cvgratlem1 7136  cvgratlem2 7137  fsum0diag4 7147  mulc1cncf 7165  ivthlem7 7173  ivthlem7OLD 7182  reeftlclt 7273  demoivre 7377  demoivreALT 7378  acdc2 7383  acdc5 7386  nn0ennn 7390  znnenlemOLD 7395  infpnlem1 7400  ruclem13 7416  infxpidmlem8 7453  infunabs 7459  infcdaabs 7460  infdif 7462  infxpabs 7464  iunctb 7468  infmap2lem2 7473  eltgt 7511  eltg2t 7512  tgval3t 7518  basgen2t 7532  subtop 7539  indistop 7541  retopbas 7548  iscld 7562  opnneiss 7621  islp2 7636  iscn 7646  iscnp 7648  cnco 7655  ismsg 7687  metreslem 7710  ssbl 7743  metcnp 7774  metcnp2 7775  ioo2bl 7799  tgioolem 7801  dscmet 7804  lmbr 7814  lmnn 7821  lmss 7836  lmclim 7846  metelcls 7848  metcnp4 7852  xplm 7857  iscms2lem4 7874  bcthlem1 7881  bcthlem17 7897  bcthlem18 7898  bcthlem19 7899  bcthlem20 7900  bcthlem21 7901  bcthlem24 7904  bcthlem25 7905  isgrp2i 7959  grplactfval 7980  ablmul 8016  ghgrpilem2 8019  ghgrpilem3 8020  ghgrpi 8022  isring 8026  ringsn 8048  isvcg 8052  vcz 8076  isnvi 8110  sqcn 8207  va1cnlem 8214  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem5 8246  nvo00 8291  nmoge0 8297  nmorepnf 8298  nmblolbii 8325  ipblnfi 8382  ubthlem3 8397  ubthlem4 8398  ubthlem5 8399  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  htthlem5 8488  htthlem6 8489  pilem2 8504  efif1lem7 8564  circgrpOLD 8571  logeftb 8599  relogexpt 8609  logeftbOLD 8619  logexptOLD 8625  lediv2itALT 8638  fiiu 8709  ficli 8727  cmphmp 8759  cnvhmpha 8763  cnvhmphb 8764  hmphsyma 8766  hmphsym 8767  hmeogrp 8776  oefil2 8791  infi 8798  cnfilca 8801  msr4 8820  mslb1 8823  iintlem1 8826  trdom 8829  cnvtr 8832  1ded 8865  isfuna 8940  hvpncan2t 9058  hvaddsub4t 9094  hiret 9109  abshicomt 9116  hial2eq2t 9122  orthcom 9123  normpyct 9162  hcau2 9205  hhcms 9223  hlimcaui 9257  ocsh 9286  occon2t 9291  chocuni 9302  projlem2 9317  projlem26 9341  pjvalt 9368  shscl 9410  shscomt 9412  shsel2t 9415  spanss 9447  shjcomt 9459  shlej1t 9484  shmods 9491  chpsscon3t 9555  spansnmul 9617  spansncol 9621  pjspansnt 9631  spanunsn 9633  cmcm2t 9690  cm2jt 9694  spansncv 9728  5oalem2 9731  3oalem2 9739  honegsubdi2t 9868  adjsymt 9890  cnvadj 9947  nmopub2tALT 9964  nmfnleub2t 9980  brafnt 10001  kbmult 10009  kbpjt 10010  nmcopexlem6 10085  lnopcon 10092  nmcfnexlem6 10114  lnfncon 10119  riesz3 10124  cnlnadjlem2 10130  cnlnadjlem9 10137  cnlnssadj 10142  nmopco 10156  cnvbravalt 10170  kbass2t 10176  kbass5t 10179  leopt 10182  leop3t 10184  leopmul2it 10194  leoptrit 10195  hmopidmch 10204  pjima 10229  cvcon3t 10335  cvnsymt 10341  mdbr2 10347  dmdmdt 10351  dmdbr2 10354  dmdbr3 10355  dmdbr4 10356  mdsl0 10359  ssmd2 10361  ssdmd1 10362  ssdmd2 10363  mdslmd1lem1 10374  mdslmd1lem2 10375  mdslmd3 10381  mdslmd4 10382  atcveq0 10397  superpos 10403  atnem0 10426  atssmat 10427  atexcht 10430  atoml 10431  atcvatlem 10434  atcvat 10435  irredlem1 10439  irredlem3 10441  irred 10443  atcvat3 10445  atdmd 10447  mdsymlem1 10452  mdsymlem3 10454  mdsymlem4 10455  mdsymlem5 10456  mdsymlem8 10459  dmdsymt 10462  sumdmdlem 10466  cdjreu 10478  cdj3lem2b 10483  cdj3 10487

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 147  df-an 225

Copyright terms: Public domain