Theorem ancoms 438

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	⊢ ((φ ⋀ ψ) → χ)

Assertion

Ref	Expression
ancoms	⊢ ((ψ ⋀ φ) → χ)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancom 437	. 2 ⊢ ((ψ ⋀ φ) ↔ (φ ⋀ ψ))
2		ancoms.1	. 2 ⊢ ((φ ⋀ ψ) → χ)
3	1, 2	sylbi 197	1 ⊢ ((ψ ⋀ φ) → χ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  anabsi8 501  anabss4 504  sylan9bbr 544  bi2anan9r 636  mpancom 709  3adantr1 812  3adantr2 813  3adantr3 814  syl3anr1 883  syl3anr2 884  syl3anr3 885  mp3anr1 919  mp3anr2 920  mp3anr3 921  2exeu 1486  2eu1 1489  2eu3 1491  eqeqan12rd 1534  sylan9eqr 1572  rcla4cva 1922  sbccomglem 2038  sbccomg 2039  csbcomg 2068  csbnestg 2088  sbcnestg 2090  sylan9ssr 2128  breqan12rd 2706  ordelssne 3002  ordtri3or 3007  ordtri2 3010  ordtri2or 3067  difex2 3101  ordunisuc2 3198  tfindsg 3213  tfindsg2 3214  dfom2 3220  ordom 3228  findsg 3245  weinxp 3319  brelrng 3430  dminss 3547  imainss 3548  coexg 3629  funeq 3640  funeu 3642  funco 3655  funcnvuni 3669  cofunex2g 3687  f1co 3774  dff1o2 3801  f1ocnv 3809  resdif 3816  funimass4 3874  fsn2 3950  isotr 4011  isotrALT 4012  opreqan12rd 4038  onopriun 4211  tfr3 4227  tz7.48-2 4258  tz7.49 4260  omcl 4307  oaordi 4316  oaword 4319  oaord1 4321  oaword2 4323  oa00 4329  oalimcl 4330  oaass 4331  oarec 4332  omord2 4334  omcan 4336  omword 4337  omword1 4340  omword2 4341  omlimcl 4345  odi 4346  omass 4347  oneo 4348  oen0 4349  oeord 4351  oecan 4352  oeword 4353  oeworde 4356  oelim2 4358  nnarcl 4372  nnaordr 4376  nnmsucr 4380  nnmcom 4381  oaabslem 4391  oaabs 4392  omsmo 4397  ersym 4412  ecopoprsym 4451  ecoprcom 4460  mapvalg 4471  pmvalg 4472  f1oeng 4536  ener 4551  domtr 4556  fundmen 4569  xpdom2 4583  ac6sfilem3 4590  onomeneq 4665  nndomo 4667  isfinite1 4677  pssnn 4681  xpfi 4685  infcntss 4699  fiint 4703  fodomfi 4709  supmaxlem 4731  suppr 4733  suc11reg 4750  inf3lem5 4762  infeq5 4766  aceq3 4879  aceq5 4886  zorn2lem6 4939  brdom3 4947  brdom7disj 4950  brdom6disj 4951  domtri 4987  sucdom 4992  unxpdom2 4995  sdomel 4997  alephord3 5028  aleph11 5029  cardaleph 5035  alephval2 5052  ltsopi 5170  mulclpi 5175  addcompi 5176  mulcompi 5178  ltapi 5184  ltmpi 5185  ordpipq 5210  ltrpq 5239  prnmadd 5254  genpnnp 5262  addcompr 5277  mulcompr 5279  ltsopr 5290  prlem934b 5292  prlem934 5293  ltexprlem2 5297  suplem1pr 5315  suplem2pr 5316  ltsrpr 5340  ssgt0sr 5371  axmulopr 5420  axmulass 5432  axdistr 5433  pre-axltadd 5443  cnegexlem3 5501  pncan3 5531  pncan2 5552  muladd 5575  subdi 5581  mulneg2 5606  negsubdi2 5612  mulsub 5631  ltxrlt 5654  xrltnle 5656  axlttri 5657  axsup 5661  ltnle 5665  letri3 5671  leloe 5672  eqlelt 5673  xrltnsym 5704  xrlttri 5706  xrleloe 5711  xrletri 5715  letric 5774  ltleadd 5799  posdif 5808  addge01 5826  suble0 5829  rec11r 5918  divadddiv 5923  divdivdiv 5924  prodgt02 5967  prodge02 5969  lemul12aOLD 5987  mulgt1 5989  ltdivmul 6011  ledivmul 6013  lt2mul2div 6016  lereci 6025  le2msqi 6027  msq11i 6028  ltdiv23 6037  lediv23 6038  lediv2a 6042  xrmaxlt 6058  maxle 6063  maxlt 6067  nnmulcl 6086  nndivtr 6106  lbreu 6213  infm3 6222  dfinfmr 6235  infmsup 6236  xrsupsslem 6244  xrinfmsslem 6245  supxr 6249  supxrunb1 6257  supxrunb2 6258  supxrbnd1 6263  nn0nnaddcl 6294  nn0sub 6329  zaddcl 6333  zrevaddcl 6338  znnsub 6345  znn0sub 6346  zltp1le 6349  z2ge 6359  zextlt 6361  gtndiv 6364  prime 6366  uzwo4OLD 6381  uzwo5OLD 6382  zmax 6392  zbtwnre 6393  rebtwnz 6394  qrevaddcl 6414  qbtwnre 6418  flge 6431  fllt 6432  flwordi 6436  flval3 6438  flbi 6439  flbi2 6440  flzadd 6444  modcyc2 6476  ioon0 6495  iooin 6498  eliooord 6514  elioc2 6516  elico2 6517  elicc2 6518  iooshf 6522  iccsupr 6525  iooneg 6533  iccneg 6534  uz11 6559  uzaddcl 6576  uzwo 6582  uzwoOLD 6583  fzen 6622  elfz2nn0 6625  fzopth 6632  fzss2 6634  fzsuc 6636  fzssp1 6637  fzrev 6642  fsequb 6654  fseqsupubi 6657  om2uzlt2i 6662  om2uzf1oi 6664  seq1rn2 6686  shftval4 6714  shftval5 6715  2shfti 6717  shftcan2 6718  seqzp1 6743  seqzval2 6748  seqzrn2 6751  ser0cl1i 6759  expcllem 6770  expsub 6793  expsubOLD 6794  expordi 6797  nn0opthi 6867  sqr2irr 6930  mulre 6978  abslti 7078  abslei 7079  abssubne0 7085  abs3dif 7102  abs2difabs 7106  seq1bndi 7113  seq1ublem 7114  cvg2i 7125  cvganz 7127  caubndi 7129  faclbnd 7148  faclbnd5 7156  facavg 7158  bccmpl 7165  bccl2 7174  fsum1i 7208  fsum1ps 7221  fsumsplit 7223  fsumshft 7234  fsumshftm 7235  fsumconst 7241  clm3i 7282  clm4lei 7284  climfnn 7295  2climnn 7305  2climnn0 7306  climge0 7315  climaddlem3 7319  climmullem1 7323  climmullem8 7330  climsubc2 7334  clim2serz 7337  climsqueeze 7343  climsqueeze2 7344  clim2serzi 7348  climserzlei 7350  caucvglem2 7361  caucvglem6 7365  caucvgi 7366  serzf0i 7372  ser1cmp2lem 7379  ser1cmp2i 7380  dfisum 7395  infcvglem1 7425  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem2 7456  fsum0diag4 7466  mulc1cncf 7484  ivthlem7 7492  reeftlcl 7585  demoivre 7695  demoivreALT 7696  acdc2 7702  acdc5 7705  nn0ennn 7709  infpnlem1 7718  ruclem13 7734  infxpidmlem8 7771  infunabs 7777  infcdaabs 7778  infdif 7780  infxpabs 7782  iunctb 7787  infmap2lem2 7792  eltg 7830  eltg2 7831  tgval3 7837  basgen2 7851  subtop 7858  retopbas 7865  iscld 7879  opnneiss 7942  islp2 7957  iscn 7968  iscnp 7970  cnco 7978  ismsg 8010  metreslem 8032  ssbl 8065  metequiv 8091  metcnp 8098  metcnp2 8099  ioo2bl 8123  tgioolem 8125  dscmet 8129  lmbr 8139  lmnn 8146  lmss 8164  lmclim 8174  metelcls 8176  metcnp4 8181  xplm 8186  iscms2lem4 8203  bcthlem1 8210  bcthlem17 8226  bcthlem18 8227  bcthlem19 8228  bcthlem20 8229  bcthlem21 8230  bcthlem24 8233  bcthlem25 8234  isgrp2i 8293  grplactfval 8337  ablmul 8372  ghgrpilem2 8375  ghgrpilem3 8376  ghgrpi 8378  isring 8382  ringideu 8387  ringsn 8405  vcz 8436  isvc 8447  isnv 8478  isnvi 8479  vacnlem3 8584  sqcn 8589  va1cnlem 8599  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem5 8631  nvo00 8678  nmoge0 8684  nmorepnf 8685  nmblolbii 8714  ipblnfi 8772  ubthlem3 8789  ubthlem4 8790  ubthlem5 8791  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  htthlem5 8886  htthlem6 8887  pslem 8909  spwval2 8915  spweu 8919  pilem2 8939  efif1lem7 9008  logeftb 9036  relogexp 9046  hvpncan2 9184  hvaddsub4 9221  hire 9236  abshicom 9243  hial2eq2 9249  orthcom 9250  normpyc 9289  hcau2 9331  hhcms 9348  hlimcauii 9382  hhssabli 9408  hhsscms 9426  ocsh 9432  occon2 9437  chocunii 9448  projlem2 9463  projlem26 9487  pjval 9515  shscli 9557  shscom 9559  shsel2 9562  spanss 9594  shjcom 9606  shlej1 9631  shmodsi 9638  chpsscon3 9702  spansnmul 9763  spansncol 9767  pjspansn 9776  spanunsni 9778  cmcm2 9835  cm2j 9839  spansncvi 9875  5oalem2 9878  3oalem2 9886  honegsubdi2 10017  adjsym 10039  cnvadj 10096  nmopub2tALT 10113  nmfnleub2 10130  brafn 10151  kbmul 10159  kbpj 10160  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem6 10264  lnfnconi 10269  riesz3i 10274  cnlnadjlem2 10280  cnlnadjlem9 10287  cnlnssadj 10292  nmopcoi 10307  cnvbraval 10323  kbass2 10330  kbass5 10333  leop 10336  leop3 10338  leopmul2i 10348  leoptri 10349  hmopidmchi 10359  pjimai 10384  cvcon3 10492  cvnsym 10498  mdbr2 10504  dmdmd 10508  dmdbr2 10511  dmdbr3 10513  dmdbr4 10514  dmdbr5 10516  mdsl0 10518  ssmd2 10520  ssdmd1 10521  ssdmd2 10522  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd3i 10540  mdslmd4i 10541  atcveq0 10556  superpos 10562  atnem0 10585  atnem0OLD 10586  atssma 10587  atexch 10590  atomli 10591  atcvatlem 10594  atcvati 10595  irredlem1 10599  irredlem3 10601  irredi 10603  atcvat3i 10605  atdmd 10607  mdsymlem1 10612  mdsymlem3 10614  mdsymlem4 10615  mdsymlem5 10616  mdsymlem8 10619  dmdsym 10622  atdmd2 10623  sumdmdlem 10627  cdjreui 10641  cdj3lem2b 10646  cdj3i 10650  lediv2aALT 10656  nndivsub 10706  nndivlub 10707  fiiu 10738  ficli 10756  domintref 10767  letri31 10791  infi 10854  ranncnt 10873  lteqtpos 10880  isdivrng 10968  cmphmp 11027  cnvhmpha 11031  cnvhmphb 11032  hmphsyma 11034  hmphsym 11035  hmeogrp 11044  hmeobc 11048  homindlem3 11053  oefil2 11079  cnfilca 11088  altretop 11144  msr4 11149  mslb1 11152  iintlem1 11155  trdom 11158  cnvtr 11161  1ded 11192  isfuna 11288  dmsdtriord 11408  elicc3 11410  ccid 11412  fiss 11419  ordtypelem5 11431  hartog 11436  omsubsuc2 11439  omsubsdom 11442  omsubdom 11443  omsubss 11445  omsubdmss 11447  omsubindss 11449  infenomsub 11450  omsubinit 11451  elsubsp 11477  subsubtop 11479  subcld 11480  subcls 11481  subntr 11482  compcov 11486  compsublem 11487  compsub 11488  compfipin0lem 11492  cncomp 11494  connsub 11502  subtopmetlem 11505  reconnlem5 11511  reconn 11512  isfne 11541  isfne3 11543  neibastop2lem3 11582  neibastop2lem4 11583  topjoin 11588  fnejoin1 11591  fgbas 11636  fgfil 11638  extbas1 11641  filrn 11643  filfinnfr 11646  ufinffr 11663  ufilen 11664  limfil 11675  flimcls 11684  fmfnfm 11704  fclusff 11735  sfclusf 11736  istail 11757  filnetlem1 11763  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  isgalem 11771  isga 11772  ssga 11777  upixp 11823  indexa 11845  indexf 11847  fipreima 11848  fimaxre 11856  filbcmb 11857  fzm1 11867  sdclem1 11875  sdclem2 11876  sdc 11877  incsequz2 11880  csbrni 11895  subspopn 11900  subspabs 11903  lpss2 11906  metf1o 11907  metsstop 11909  mettrifi2 11913  geomcau 11914  iccsplit 11919  lincmb01cmp 11942  lincmb01icc 11943  addccncf 11945  sub1cncf 11946  sub2cncf 11947  cnimass 11949  cnres 11950  cnresima 11952  cnss 11953  haustlmu 11967  lmtlm 11969  uptx 11978  txcn 11979  txcnopab 11980  txsubsp 11983  sstotbnd 11992  totbndss 11993  isbnd3 11997  bndss 11998  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtybnd 12009  ismtyres 12010  heiborlem1 12011  heiborlem16 12026  heiborlem18 12028  heiborlem23 12033  heiborlem28 12038  bfplem8 12061  bfp 12065  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  phtpycom 12092

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 145  df-an 223

Copyright terms: Public domain