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 703  3adantr1 804  3adantr2 805  3adantr3 806  syl3anr1 874  syl3anr2 875  syl3anr3 876  mp3anr1 910  mp3anr2 911  mp3anr3 912  2exeu 1439  2eu1 1442  2eu3 1444  eqeqan12rd 1483  sylan9eqr 1521  rcla4cva 1867  sbccomglem 1978  sbccomg 1979  csbcomg 2007  csbnestg 2026  sbcnestg 2028  sylan9ssr 2066  breqan12rd 2623  difex2 2867  ordelssne 2964  ordtri3or 2969  ordtri2 2972  ordtri2or 3067  ordunisuc2 3105  dfom2 3123  ordom 3131  findsg 3147  tfindsg 3152  tfindsg2 3153  weinxp 3223  dminss 3448  imainss 3449  coexg 3510  funeq 3521  funeu 3523  funco 3536  funcnvuni 3550  cofunex2g 3567  f1co 3652  f1o2 3678  f1ocnv 3686  funimass4 3748  fsn2 3821  isotr 3882  isotrALT 3883  tfr3 3911  tz7.48-2 3942  tz7.49 3944  opreqan12rd 3965  omcl 4155  oaordi 4164  oaword 4167  oaord1 4169  oaword2 4171  oa00 4177  oalimcl 4178  oaass 4179  oarec 4180  omord2 4182  omcan 4184  omword 4185  omword1 4188  omword2 4189  omlimcl 4193  odi 4194  omass 4195  oneo 4196  oen0 4197  oeord 4199  oecan 4200  oeword 4201  oeworde 4204  oelim2 4206  nnarcl 4216  nnaordr 4220  nnmsucr 4224  nnmcom 4225  oaabslem 4235  oaabs 4236  omsmo 4241  ersym 4256  ecopoprsym 4294  ecoprcom 4303  mapvalg 4314  pmvalg 4315  f1oeng 4376  ener 4391  domtr 4396  fundmen 4409  xpdom2 4422  onomeneq 4498  nndomo 4500  isfinite1 4510  pssnn 4513  infcntss 4530  fiint 4534  fodomfi 4540  suppr 4562  suc11reg 4577  inf3lem5 4589  infeq5 4593  aceq3 4705  aceq5 4712  zorn2lem6 4765  brdom3 4773  brdom7disj 4776  brdom6disj 4777  domtri 4810  sucdom 4814  unxpdom2 4817  sdomel 4819  alephord3 4850  aleph11 4851  cardaleph 4857  alephval2 4874  ltsopi 4988  mulclpi 4993  addcompi 4994  mulcompi 4996  ltapi 5002  ltmpi 5003  ordpipq 5028  ltrpq 5057  prnmadd 5072  genpnnp 5080  addcompr 5095  mulcompr 5097  ltsopr 5108  prlem934b 5110  prlem934 5111  ltexprlem2 5115  suplem1pr 5133  suplem2pr 5134  ltsrpr 5158  ssgt0sr 5189  axmulopr 5238  axmulass 5250  axdistr 5251  pre-axltadd 5261  cnegextlem3 5319  pncan3t 5349  pncan2t 5370  muladdt 5393  subdit 5399  mulneg2t 5424  negsubdi2t 5430  mulsubt 5449  ltxrltt 5472  xrltnlet 5474  axlttri 5475  axsup 5479  ltnlet 5483  letri3t 5490  leloet 5491  eqleltt 5492  xrltnsymt 5523  xrlttrit 5525  xrleloet 5530  xrletrit 5534  letrit 5594  ltleaddt 5619  posdift 5627  addge01t 5645  suble0t 5648  divcan5t 5737  divdivdivt 5741  prodgt02t 5783  prodge02t 5785  lemul12itOLD 5799  mulgt1t 5801  lerec 5828  le2msq 5830  msq11 5831  ltdiv23t 5840  lediv23t 5841  lediv2it 5845  xrmaxltt 5861  maxlet 5866  maxltt 5870  nnmulclt 5889  nndivtrt 5907  lbreu 5992  infm3 6001  dfinfmr 6014  infmsup 6015  xrsupsslem 6023  xrinfmsslem 6024  supxr 6028  supxrunb1 6036  supxrunb2 6037  supxrbnd1 6042  nn0nnaddclt 6073  nn0subt 6108  zaddclt 6112  zrevaddclt 6117  znnsubt 6124  znn0subt 6125  zltp1let 6128  z2get 6135  zextltt 6137  gtndivt 6140  primet 6142  uzwo4OLD 6158  uzwo5OLD 6159  zmax 6168  zbtwnre 6169  rebtwnz 6170  flget 6178  flltt 6179  flval3t 6182  flwordit 6183  flbit 6184  qrevaddclt 6213  qbtwnre 6216  om2uzlt2 6236  om2uzf1o 6238  seq1rn2 6258  shftval4t 6286  shftval5t 6287  2shft 6289  shftcan2t 6290  ioon0t 6306  iooint 6309  elioc2t 6322  elico2t 6323  elicc2t 6324  ioossicc 6330  iccsupr 6331  ioonegt 6339  iccnegt 6340  uz11t 6364  uzaddclt 6381  uzwo 6387  uzwoOLD 6388  elfz2nn0t 6427  fzoptht 6434  fzss2t 6436  fzssp1t 6438  fzrevt 6443  fsequb 6455  fseqsupub 6458  seqzp1 6480  seqzval2t 6485  seqzrn2 6488  ser0cl1 6496  expcllem 6507  expsubt 6529  expordit 6531  nn0opth 6596  sqr2irr 6659  abslt 6810  absle 6811  abssubne0t 6820  abs3dift 6836  abs2difabst 6840  seq1bnd 6847  seq1ublem 6848  cvg2 6859  cvganz 6861  caubnd 6863  faclbnd 6882  faclbnd5 6890  facavgt 6892  bccmplt 6900  bccl2t 6909  fsum1 6943  fsum1ps 6956  fsumsplit 6958  fsumshft 6969  fsumshftm 6970  fsumconst 6976  clm3 7017  clm4le 7019  climfnn 7030  2climnn 7039  2climnn0 7040  climge0 7049  climaddlem3 7052  climmullem1 7056  climmullem8 7063  climsubc2 7067  clim2serzt 7070  climsqueeze 7076  climsqueeze2 7077  clim2serz 7081  climserzle 7083  caucvglem2 7094  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp2lem 7112  ser1cmp2 7113  dfisum 7127  infcvglem1 7156  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  fsum0diag4 7196  mulc1cncf 7214  ivthlem7 7222  ivthlem7OLD 7231  reeftlclt 7322  demoivre 7426  demoivreALT 7427  acdc2 7432  acdc5 7435  nn0ennn 7439  znnenlemOLD 7444  infpnlem1 7449  ruclem13 7465  infxpidmlem8 7502  infunabs 7508  infcdaabs 7509  infdif 7511  infxpabs 7513  iunctb 7517  infmap2lem2 7522  eltgt 7560  eltg2t 7561  tgval3t 7567  basgen2t 7581  subtop 7588  indistop 7590  retopbas 7597  iscld 7611  opnneiss 7673  islp2 7688  iscn 7698  iscnp 7700  cnco 7707  ismsg 7739  metreslem 7762  ssbl 7795  metcnp 7826  metcnp2 7827  ioo2bl 7851  tgioolem 7853  dscmet 7856  lmbr 7866  lmnn 7873  lmss 7888  lmclim 7898  metelcls 7900  metcnp4 7904  xplm 7909  iscms2lem4 7926  bcthlem1 7933  bcthlem17 7949  bcthlem18 7950  bcthlem19 7951  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  isgrp2i 8011  grplactfval 8032  ablmul 8068  ghgrpilem2 8071  ghgrpilem3 8072  ghgrpi 8074  isring 8078  ringsn 8100  vcz 8126  isvcgOLD 8133  isvc 8138  isnv 8170  isnvi 8171  isnviOLD 8172  sqcn 8270  va1cnlem 8279  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem5 8311  nvo00 8356  nmoge0 8362  nmorepnf 8363  nmblolbii 8390  ipblnfi 8447  ubthlem3 8462  ubthlem4 8463  ubthlem5 8464  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  htthlem5 8554  htthlem6 8555  pslem 8573  spwval2 8577  spweu 8581  pilem2 8591  efif1lem7 8651  circgrpOLD 8658  logeftb 8686  relogexpt 8696  logeftbOLD 8706  logexptOLD 8712  hvpncan2t 8830  hvaddsub4t 8866  hiret 8881  abshicomt 8888  hial2eq2t 8894  orthcom 8895  normpyct 8934  hcau2 8976  hhcms 8993  hlimcaui 9027  hhssabl 9053  hhsscms 9067  ocsh 9072  occon2t 9077  chocuni 9088  projlem2 9103  projlem26 9127  pjvalt 9154  shscl 9196  shscomt 9198  shsel2t 9201  spanss 9233  shjcomt 9245  shlej1t 9270  shmods 9277  chpsscon3t 9341  spansnmul 9403  spansncol 9407  pjspansnt 9417  spanunsn 9419  cmcm2t 9476  cm2jt 9480  spansncv 9514  5oalem2 9517  3oalem2 9525  honegsubdi2t 9654  adjsymt 9676  cnvadj 9733  nmopub2tALT 9750  nmfnleub2t 9766  brafnt 9787  kbmult 9795  kbpjt 9796  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem6 9900  lnfncon 9905  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem9 9923  cnlnssadj 9928  nmopco 9942  cnvbravalt 9956  kbass2t 9962  kbass5t 9965  leopt 9968  leop3t 9970  leopmul2it 9980  leoptrit 9981  hmopidmch 9990  pjima 10015  cvcon3t 10121  cvnsymt 10127  mdbr2 10133  dmdmdt 10137  dmdbr2 10140  dmdbr3 10141  dmdbr4 10142  mdsl0 10145  ssmd2 10147  ssdmd1 10148  ssdmd2 10149  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd3 10167  mdslmd4 10168  atcveq0 10183  superpos 10189  atnem0 10212  atssmat 10213  atexcht 10216  atoml 10217  atcvatlem 10220  atcvat 10221  irredlem1 10225  irredlem3 10227  irred 10229  atcvat3 10231  atdmd 10233  mdsymlem1 10238  mdsymlem3 10240  mdsymlem4 10241  mdsymlem5 10242  mdsymlem8 10245  dmdsymt 10248  sumdmdlem 10252  cdjreu 10264  cdj3lem2b 10269  cdj3 10273  lediv2itALT 10276  fiiu 10350  ficli 10368  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  hmphsyma 10415  hmphsym 10416  hmeogrp 10425  oefil2 10441  infi 10448  cnfilca 10451  msr4 10470  mslb1 10473  iintlem1 10476  trdom 10479  cnvtr 10482  1ded 10515  isfuna 10592

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