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 498  anabss4 501  sylan9bbr 541  bi2anan9r 633  mpancom 705  3adantr1 806  3adantr2 807  3adantr3 808  syl3anr1 877  syl3anr2 878  syl3anr3 879  mp3anr1 913  mp3anr2 914  mp3anr3 915  2exeu 1446  2eu1 1449  2eu3 1451  eqeqan12rd 1491  sylan9eqr 1529  rcla4cva 1876  sbccomglem 1988  sbccomg 1989  csbcomg 2017  csbnestg 2036  sbcnestg 2038  sylan9ssr 2076  breqan12rd 2633  difex2 2877  ordelssne 2974  ordtri3or 2979  ordtri2 2982  ordtri2or 3077  ordunisuc2 3115  dfom2 3133  ordom 3141  findsg 3157  tfindsg 3162  tfindsg2 3163  weinxp 3233  brelrng 3343  dminss 3462  imainss 3463  coexg 3524  funeq 3535  funeu 3537  funco 3550  funcnvuni 3564  cofunex2g 3581  f1co 3667  f1o2 3693  f1ocnv 3701  funimass4 3763  fsn2 3836  isotr 3897  isotrALT 3898  tfr3 3926  tz7.48-2 3957  tz7.49 3959  opreqan12rd 3980  omcl 4171  oaordi 4180  oaword 4183  oaord1 4185  oaword2 4187  oa00 4193  oalimcl 4194  oaass 4195  oarec 4196  omord2 4198  omcan 4200  omword 4201  omword1 4204  omword2 4205  omlimcl 4209  odi 4210  omass 4211  oneo 4212  oen0 4213  oeord 4215  oecan 4216  oeword 4217  oeworde 4220  oelim2 4222  nnarcl 4232  nnaordr 4236  nnmsucr 4240  nnmcom 4241  oaabslem 4251  oaabs 4252  omsmo 4257  ersym 4272  ecopoprsym 4310  ecoprcom 4319  mapvalg 4330  pmvalg 4331  f1oeng 4395  ener 4410  domtr 4415  fundmen 4428  xpdom2 4442  onomeneq 4519  nndomo 4521  isfinite1OLD 4531  pssnn 4534  infcntss 4554  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  supmaxlem 4588  suppr 4590  suc11reg 4605  inf3lem5 4617  infeq5 4621  aceq3 4733  aceq5 4740  zorn2lem6 4793  brdom3 4801  brdom7disj 4804  brdom6disj 4805  domtri 4838  sucdom 4842  unxpdom2 4845  sdomel 4847  alephord3 4878  aleph11 4879  cardaleph 4885  alephval2 4902  ltsopi 5016  mulclpi 5021  addcompi 5022  mulcompi 5024  ltapi 5030  ltmpi 5031  ordpipq 5056  ltrpq 5085  prnmadd 5100  genpnnp 5108  addcompr 5123  mulcompr 5125  ltsopr 5136  prlem934b 5138  prlem934 5139  ltexprlem2 5143  suplem1pr 5161  suplem2pr 5162  ltsrpr 5186  ssgt0sr 5217  axmulopr 5266  axmulass 5278  axdistr 5279  pre-axltadd 5289  cnegextlem3 5347  pncan3t 5377  pncan2t 5398  muladdt 5421  subdit 5427  mulneg2t 5452  negsubdi2t 5458  mulsubt 5477  ltxrltt 5500  xrltnlet 5502  axlttri 5503  axsup 5507  ltnlet 5511  letri3t 5517  leloet 5518  eqleltt 5519  xrltnsymt 5550  xrlttrit 5552  xrleloet 5557  xrletrit 5561  letrit 5620  ltleaddt 5645  posdift 5654  addge01t 5672  suble0t 5675  divcan5t 5781  divdivdivt 5785  prodgt02t 5827  prodge02t 5829  lemul12itOLD 5843  mulgt1t 5845  ltdivmult 5867  lerec 5880  le2msq 5882  msq11 5883  ltdiv23t 5892  lediv23t 5893  lediv2it 5897  xrmaxltt 5913  maxlet 5918  maxltt 5922  nnmulclt 5941  nndivtrt 5960  lbreu 6045  infm3 6054  dfinfmr 6067  infmsup 6068  xrsupsslem 6076  xrinfmsslem 6077  supxr 6081  supxrunb1 6089  supxrunb2 6090  supxrbnd1 6095  nn0nnaddclt 6126  nn0subt 6161  zaddclt 6165  zrevaddclt 6170  znnsubt 6177  znn0subt 6178  zltp1let 6181  z2get 6188  zextltt 6190  gtndivt 6193  primet 6195  uzwo4OLD 6210  uzwo5OLD 6211  zmax 6220  zbtwnre 6221  rebtwnz 6222  flget 6233  flltt 6234  flwordit 6237  flval3t 6239  flbit 6240  flbi2t 6241  qrevaddclt 6275  qbtwnre 6278  om2uzlt2 6299  om2uzf1o 6301  seq1rn2 6321  shftval4t 6349  shftval5t 6350  2shft 6352  shftcan2t 6353  ioon0t 6369  iooint 6372  eliooordt 6388  elioc2t 6390  elico2t 6391  elicc2t 6392  iccsupr 6398  ioonegt 6406  iccnegt 6407  uz11t 6432  uzaddclt 6449  uzwo 6455  uzwoOLD 6456  elfz2nn0t 6495  fzoptht 6502  fzss2t 6504  fzssp1t 6506  fzrevt 6511  fsequb 6523  fseqsupub 6526  seqzp1 6548  seqzval2t 6553  seqzrn2 6556  ser0cl1 6564  expcllem 6575  expsubt 6598  expordit 6600  nn0opth 6666  sqr2irr 6729  abslt 6875  absle 6876  abssubne0t 6882  abs3dift 6899  abs2difabst 6903  seq1bnd 6910  seq1ublem 6911  cvg2 6922  cvganz 6924  caubnd 6926  faclbnd 6945  faclbnd5 6953  facavgt 6955  bccmplt 6962  bccl2t 6971  fsum1 7005  fsum1ps 7018  fsumsplit 7020  fsumshft 7031  fsumshftm 7032  fsumconst 7038  clm3 7079  clm4le 7081  climfnn 7092  2climnn 7102  2climnn0 7103  climge0 7112  climaddlem3 7116  climmullem1 7120  climmullem8 7127  climsubc2 7131  clim2serzt 7134  climsqueeze 7140  climsqueeze2 7141  clim2serz 7145  climserzle 7147  caucvglem2 7158  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp2lem 7176  ser1cmp2 7177  dfisum 7191  infcvglem1 7221  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  fsum0diag4 7261  mulc1cncf 7279  ivthlem7 7287  reeftlclt 7380  demoivre 7484  demoivreALT 7485  acdc2 7490  acdc5 7493  nn0ennn 7497  infpnlem1 7506  ruclem13 7522  infxpidmlem8 7559  infunabs 7565  infcdaabs 7566  infdif 7568  infxpabs 7570  iunctb 7575  infmap2lem2 7580  eltgt 7618  eltg2t 7619  tgval3t 7625  basgen2t 7639  subtop 7646  indistop 7648  retopbas 7655  iscld 7669  opnneiss 7732  islp2 7747  iscn 7758  iscnp 7760  cnco 7768  ismsg 7800  metreslem 7822  ssbl 7855  metcnp 7887  metcnp2 7888  ioo2bl 7912  tgioolem 7914  dscmet 7918  lmbr 7928  lmnn 7935  lmss 7953  lmclim 7963  metelcls 7965  metcnp4 7970  xplm 7975  iscms2lem4 7992  bcthlem1 7999  bcthlem17 8015  bcthlem18 8016  bcthlem19 8017  bcthlem20 8018  bcthlem21 8019  bcthlem24 8022  bcthlem25 8023  isgrp2i 8076  grplactfval 8096  ablmul 8131  ghgrpilem2 8134  ghgrpilem3 8135  ghgrpi 8137  isring 8141  ringsn 8163  vcz 8189  isvc 8200  isnv 8231  isnvi 8232  sqcn 8335  va1cnlem 8345  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem5 8377  nvo00 8424  nmoge0 8430  nmorepnf 8431  nmblolbii 8459  ipblnfi 8516  ubthlem3 8531  ubthlem4 8532  ubthlem5 8533  ubthlem11 8539  ubthlem12 8540  ubthlem13 8541  ubthlem14 8542  htthlem5 8624  htthlem6 8625  pslem 8647  spwval2 8653  spweu 8657  pilem2 8672  efif1lem7 8736  logeftb 8764  relogexpt 8774  hvpncan2t 8909  hvaddsub4t 8945  hiret 8960  abshicomt 8967  hial2eq2t 8973  orthcom 8974  normpyct 9013  hcau2 9055  hhcms 9072  hlimcaui 9106  hhssabl 9132  hhsscms 9150  ocsh 9156  occon2t 9161  chocuni 9172  projlem2 9187  projlem26 9211  pjvalt 9239  shscl 9281  shscomt 9283  shsel2t 9286  spanss 9318  shjcomt 9330  shlej1t 9355  shmods 9362  chpsscon3t 9426  spansnmul 9487  spansncol 9491  pjspansnt 9500  spanunsn 9502  cmcm2t 9559  cm2jt 9563  spansncv 9597  5oalem2 9600  3oalem2 9608  honegsubdi2t 9737  adjsymt 9759  cnvadj 9816  nmopub2tALT 9833  nmfnleub2t 9850  brafnt 9871  kbmult 9879  kbpjt 9880  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem6 9985  lnfncon 9990  riesz3 9995  cnlnadjlem2 10001  cnlnadjlem9 10008  cnlnssadj 10013  nmopco 10028  cnvbravalt 10043  kbass2t 10050  kbass5t 10053  leopt 10056  leop3t 10058  leopmul2it 10068  leoptrit 10069  hmopidmch 10079  pjima 10104  cvcon3t 10211  cvnsymt 10217  mdbr2 10223  dmdmdt 10227  dmdbr2 10230  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdsl0 10237  ssmd2 10239  ssdmd1 10240  ssdmd2 10241  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd3 10259  mdslmd4 10260  atcveq0 10275  superpos 10281  atnem0 10304  atssmat 10305  atexcht 10308  atoml 10309  atcvatlem 10312  atcvat 10313  irredlem1 10317  irredlem3 10319  irred 10321  atcvat3 10323  atdmd 10325  mdsymlem1 10330  mdsymlem3 10332  mdsymlem4 10333  mdsymlem5 10334  mdsymlem8 10337  dmdsymt 10340  atdmd2 10341  sumdmdlem 10345  cdjreu 10359  cdj3lem2b 10364  cdj3 10368  lediv2itALT 10371  nndivsub 10421  nndivlub 10422  fiiu 10453  fiiuOLD 10454  ficli 10472  ficliOLD 10473  cmphmp 10521  cnvhmpha 10525  cnvhmphb 10526  hmphsyma 10528  hmphsym 10529  hmeogrp 10538  hmeobc 10542  homindlem3 10551  oefil2 10567  infi 10578  infiOLD 10579  cnfilca 10583  cnfilcaOLD 10584  msr4 10626  mslb1 10629  iintlem1 10632  trdom 10635  cnvtr 10638  1ded 10671  isfuna 10754

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