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

Assertion

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

Proof of Theorem ancoms

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

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  anabsi8 498  anabss4 501  sylan9bbr 540  bi2anan9r 632  mpancom 704  3adantr1 805  3adantr2 806  3adantr3 807  syl3anr1 875  syl3anr2 876  syl3anr3 877  mp3anr1 911  mp3anr2 912  mp3anr3 913  2exeu 1444  2eu1 1447  2eu3 1449  eqeqan12rd 1488  sylan9eqr 1526  rcla4cva 1872  sbccomglem 1984  sbccomg 1985  csbcomg 2013  csbnestg 2032  sbcnestg 2034  sylan9ssr 2072  breqan12rd 2628  difex2 2872  ordelssne 2969  ordtri3or 2974  ordtri2 2977  ordtri2or 3072  ordunisuc2 3110  dfom2 3128  ordom 3136  findsg 3152  tfindsg 3157  tfindsg2 3158  weinxp 3228  brelrng 3338  dminss 3454  imainss 3455  coexg 3516  funeq 3527  funeu 3529  funco 3542  funcnvuni 3556  cofunex2g 3573  f1co 3658  f1o2 3684  f1ocnv 3692  funimass4 3754  fsn2 3827  isotr 3888  isotrALT 3889  tfr3 3917  tz7.48-2 3948  tz7.49 3950  opreqan12rd 3971  omcl 4161  oaordi 4170  oaword 4173  oaord1 4175  oaword2 4177  oa00 4183  oalimcl 4184  oaass 4185  oarec 4186  omord2 4188  omcan 4190  omword 4191  omword1 4194  omword2 4195  omlimcl 4199  odi 4200  omass 4201  oneo 4202  oen0 4203  oeord 4205  oecan 4206  oeword 4207  oeworde 4210  oelim2 4212  nnarcl 4222  nnaordr 4226  nnmsucr 4230  nnmcom 4231  oaabslem 4241  oaabs 4242  omsmo 4247  ersym 4262  ecopoprsym 4300  ecoprcom 4309  mapvalg 4320  pmvalg 4321  f1oeng 4382  ener 4397  domtr 4402  fundmen 4415  xpdom2 4428  onomeneq 4504  nndomo 4506  isfinite1 4516  pssnn 4519  infcntss 4536  fiint 4540  fodomfi 4546  supmaxlem 4568  suppr 4570  suc11reg 4585  inf3lem5 4597  infeq5 4601  aceq3 4713  aceq5 4720  zorn2lem6 4773  brdom3 4781  brdom7disj 4784  brdom6disj 4785  domtri 4818  sucdom 4822  unxpdom2 4825  sdomel 4827  alephord3 4858  aleph11 4859  cardaleph 4865  alephval2 4882  ltsopi 4996  mulclpi 5001  addcompi 5002  mulcompi 5004  ltapi 5010  ltmpi 5011  ordpipq 5036  ltrpq 5065  prnmadd 5080  genpnnp 5088  addcompr 5103  mulcompr 5105  ltsopr 5116  prlem934b 5118  prlem934 5119  ltexprlem2 5123  suplem1pr 5141  suplem2pr 5142  ltsrpr 5166  ssgt0sr 5197  axmulopr 5246  axmulass 5258  axdistr 5259  pre-axltadd 5269  cnegextlem3 5327  pncan3t 5357  pncan2t 5378  muladdt 5401  subdit 5407  mulneg2t 5432  negsubdi2t 5438  mulsubt 5457  ltxrltt 5480  xrltnlet 5482  axlttri 5483  axsup 5487  ltnlet 5491  letri3t 5498  leloet 5499  eqleltt 5500  xrltnsymt 5531  xrlttrit 5533  xrleloet 5538  xrletrit 5542  letrit 5602  ltleaddt 5627  posdift 5635  addge01t 5653  suble0t 5656  divcan5t 5745  divdivdivt 5749  prodgt02t 5791  prodge02t 5793  lemul12itOLD 5807  mulgt1t 5809  lerec 5836  le2msq 5838  msq11 5839  ltdiv23t 5848  lediv23t 5849  lediv2it 5853  xrmaxltt 5869  maxlet 5874  maxltt 5878  nnmulclt 5897  nndivtrt 5915  lbreu 6000  infm3 6009  dfinfmr 6022  infmsup 6023  xrsupsslem 6031  xrinfmsslem 6032  supxr 6036  supxrunb1 6044  supxrunb2 6045  supxrbnd1 6050  nn0nnaddclt 6081  nn0subt 6116  zaddclt 6120  zrevaddclt 6125  znnsubt 6132  znn0subt 6133  zltp1let 6136  z2get 6143  zextltt 6145  gtndivt 6148  primet 6150  uzwo4OLD 6166  uzwo5OLD 6167  zmax 6176  zbtwnre 6177  rebtwnz 6178  flget 6186  flltt 6187  flval3t 6190  flwordit 6191  flbit 6192  qrevaddclt 6221  qbtwnre 6224  om2uzlt2 6244  om2uzf1o 6246  seq1rn2 6266  shftval4t 6294  shftval5t 6295  2shft 6297  shftcan2t 6298  ioon0t 6314  iooint 6317  elioc2t 6330  elico2t 6331  elicc2t 6332  ioossicc 6338  iccsupr 6339  ioonegt 6347  iccnegt 6348  uz11t 6372  uzaddclt 6389  uzwo 6395  uzwoOLD 6396  elfz2nn0t 6435  fzoptht 6442  fzss2t 6444  fzssp1t 6446  fzrevt 6451  fsequb 6463  fseqsupub 6466  seqzp1 6488  seqzval2t 6493  seqzrn2 6496  ser0cl1 6504  expcllem 6515  expsubt 6537  expordit 6539  nn0opth 6604  sqr2irr 6667  abslt 6818  absle 6819  abssubne0t 6828  abs3dift 6844  abs2difabst 6848  seq1bnd 6855  seq1ublem 6856  cvg2 6867  cvganz 6869  caubnd 6871  faclbnd 6890  faclbnd5 6898  facavgt 6900  bccmplt 6908  bccl2t 6917  fsum1 6951  fsum1ps 6964  fsumsplit 6966  fsumshft 6977  fsumshftm 6978  fsumconst 6984  clm3 7025  clm4le 7027  climfnn 7038  2climnn 7047  2climnn0 7048  climge0 7057  climaddlem3 7060  climmullem1 7064  climmullem8 7071  climsubc2 7075  clim2serzt 7078  climsqueeze 7084  climsqueeze2 7085  clim2serz 7089  climserzle 7091  caucvglem2 7102  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp2lem 7120  ser1cmp2 7121  dfisum 7135  infcvglem1 7164  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem2 7194  fsum0diag4 7204  mulc1cncf 7222  ivthlem7 7230  ivthlem7OLD 7239  reeftlclt 7330  demoivre 7434  demoivreALT 7435  acdc2 7440  acdc5 7443  nn0ennn 7447  znnenlemOLD 7452  infpnlem1 7457  ruclem13 7473  infxpidmlem8 7510  infunabs 7516  infcdaabs 7517  infdif 7519  infxpabs 7521  iunctb 7525  infmap2lem2 7530  eltgt 7568  eltg2t 7569  tgval3t 7575  basgen2t 7589  subtop 7596  indistop 7598  retopbas 7605  iscld 7619  opnneiss 7682  islp2 7697  iscn 7708  iscnp 7710  cnco 7718  ismsg 7750  metreslem 7774  ssbl 7807  metcnp 7839  metcnp2 7840  ioo2bl 7864  tgioolem 7866  dscmet 7870  lmbr 7880  lmnn 7887  lmss 7904  lmclim 7914  metelcls 7916  metcnp4 7920  xplm 7925  iscms2lem4 7942  bcthlem1 7949  bcthlem17 7965  bcthlem18 7966  bcthlem19 7967  bcthlem20 7968  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  isgrp2i 8026  grplactfval 8047  ablmul 8083  ghgrpilem2 8086  ghgrpilem3 8087  ghgrpi 8089  isring 8093  ringsn 8115  vcz 8141  isvc 8152  isnv 8183  isnvi 8184  sqcn 8283  va1cnlem 8292  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem5 8324  nvo00 8369  nmoge0 8375  nmorepnf 8376  nmblolbii 8403  ipblnfi 8460  ubthlem3 8475  ubthlem4 8476  ubthlem5 8477  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  htthlem5 8567  htthlem6 8568  pslem 8590  spwval2 8595  spweu 8599  pilem2 8610  efif1lem7 8670  circgrpOLD 8677  logeftb 8703  relogexpt 8713  hvpncan2t 8848  hvaddsub4t 8884  hiret 8899  abshicomt 8906  hial2eq2t 8912  orthcom 8913  normpyct 8952  hcau2 8994  hhcms 9011  hlimcaui 9045  hhssabl 9071  hhsscms 9089  ocsh 9095  occon2t 9100  chocuni 9111  projlem2 9126  projlem26 9150  pjvalt 9177  shscl 9219  shscomt 9221  shsel2t 9224  spanss 9256  shjcomt 9268  shlej1t 9293  shmods 9300  chpsscon3t 9364  spansnmul 9426  spansncol 9430  pjspansnt 9440  spanunsn 9442  cmcm2t 9499  cm2jt 9503  spansncv 9537  5oalem2 9540  3oalem2 9548  honegsubdi2t 9677  adjsymt 9699  cnvadj 9756  nmopub2tALT 9773  nmfnleub2t 9789  brafnt 9810  kbmult 9818  kbpjt 9819  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem6 9923  lnfncon 9928  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem9 9946  cnlnssadj 9951  nmopco 9966  cnvbravalt 9981  kbass2t 9988  kbass5t 9991  leopt 9994  leop3t 9996  leopmul2it 10006  leoptrit 10007  hmopidmch 10017  pjima 10042  cvcon3t 10149  cvnsymt 10155  mdbr2 10161  dmdmdt 10165  dmdbr2 10168  dmdbr3 10170  dmdbr4 10171  mdsl0 10174  ssmd2 10176  ssdmd1 10177  ssdmd2 10178  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd3 10196  mdslmd4 10197  atcveq0 10212  superpos 10218  atnem0 10241  atssmat 10242  atexcht 10245  atoml 10246  atcvatlem 10249  atcvat 10250  irredlem1 10254  irredlem3 10256  irred 10258  atcvat3 10260  atdmd 10262  mdsymlem1 10267  mdsymlem3 10269  mdsymlem4 10270  mdsymlem5 10271  mdsymlem8 10274  dmdsymt 10277  sumdmdlem 10281  cdjreu 10293  cdj3lem2b 10298  cdj3 10302  lediv2itALT 10305  nndivsub 10357  nndivlub 10358  fiiu 10386  ficli 10404  cmphmp 10444  cnvhmpha 10448  cnvhmphb 10449  hmphsyma 10451  hmphsym 10452  hmeogrp 10461  oefil2 10477  infi 10484  cnfilca 10487  msr4 10506  mslb1 10509  iintlem1 10512  trdom 10515  cnvtr 10518  1ded 10551  isfuna 10628

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