MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an32s Structured version   Unicode version

Theorem an32s 802
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
an32s  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )

Proof of Theorem an32s
StepHypRef Expression
1 an32 796 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 195 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  anass1rs  805  anabss1  812  wereu2  4865  ordintdif  4916  ordunisssuc  4969  sossfld  5438  fssres  5733  foco  5787  dffv2  5921  fconstfvOLD  6109  isocnv  6201  f1oiso  6222  f1ocnvfv3  6266  fun11iun  6733  onfununi  7004  oev2  7165  oaordi  7187  oaass  7202  omlimcl  7219  odi  7220  omass  7221  oewordri  7233  oelim2  7236  oeoa  7238  oeoe  7240  nnaordi  7259  omabs  7288  eceqoveq  7408  mapxpen  7676  mapdom2  7681  dif1en  7745  findcard  7751  fimax2g  7758  isfinite2  7770  rankval3b  8235  isf32lem9  8732  fin1a2s  8785  zornn0g  8876  gchen1  8992  gchen2  8993  intwun  9102  suplem2pr  9420  recexsrlem  9469  axpre-sup  9535  axsup  9649  dedekind  9733  recextlem2  10176  divne0  10215  dfinfmr  10515  uzindOLD  10953  qreccl  11203  xrlttr  11349  xaddf  11426  xrsupsslem  11501  xrinfmsslem  11502  supxr2  11508  supxrunb1  11514  supxrbnd1  11516  supxrbnd2  11517  modid  12003  seqof  12149  cau3lem  13272  lo1bdd2  13432  o1co  13494  rlimcn2  13498  climcn1  13499  climcn2  13500  rlimsqzlem  13556  caucvgb  13587  fsumrlim  13710  fsumo1  13711  ntrivcvg  13791  rplpwr  14281  dvdssq  14285  nn0seqcvgd  14286  isprm2lem  14311  isprm6  14337  phiprmpw  14393  pcneg  14484  prmpwdvds  14509  4sqlem19  14568  0ramcl  14628  imasleval  15033  catpropd  15200  funcres2c  15392  initoeu2  15497  acsfiindd  16009  latdisdlem  16021  dirtr  16068  mrcmndind  16199  grpinveu  16286  mulgnn0subcl  16357  mulgsubcl  16358  mhmmulg  16376  cycsubgcl  16429  cycsubgss  16430  ghmmulg  16481  odf1  16786  dfod2  16788  gexdvds2  16807  sylow2blem3  16844  frgpup1  16995  iscyggen2  17086  iscyg3  17091  prdsgsum  17205  prdsgsumOLD  17206  ringrghm  17449  dvdsrcl2  17497  crngunit  17509  dvdsrpropd  17543  lss1d  17807  quscrng  18086  coe1tmmul  18516  mulgghm2  18712  frgpcyg  18788  ip0r  18848  isphld  18865  frlmgsumOLD  18975  frlmgsum  18976  uvcresum  18998  mdetdiagid  19272  cpmatmcllem  19389  tgcl  19641  0ntr  19742  innei  19796  neitr  19851  ordtrest2lem  19874  cncnp  19951  cnnei  19953  2ndcdisj  20126  dislly  20167  dissnlocfin  20199  kgenss  20213  ptcnplem  20291  ptcnp  20292  ptcn  20297  cnmpt2k  20358  qtoprest  20387  kqt0lem  20406  isr0  20407  kqreglem1  20411  trfilss  20559  isufil2  20578  ufileu  20589  hausflim  20651  cnextcn  20736  symgtgp  20769  tsmssubm  20813  tsmsxplem1  20824  ustfilxp  20884  ustuqtop0  20912  elbl2ps  21061  elbl2  21062  nrginvrcn  21369  nmoix  21405  nmoleub  21407  cncfco  21580  icccvx  21619  iscmet3  21901  rrxmet  22004  ovolfioo  22048  ovolficc  22049  ovolicc2lem4  22100  iunmbl2  22136  dyadmax  22176  mbfsup  22240  mbflimsup  22242  mbflim  22244  itg1addlem4  22275  mbfi1flimlem  22298  itg2monolem1  22326  itg2mono  22329  itg2i1fseqle  22330  itg2i1fseq  22331  itg2addlem  22334  itg2gt0  22336  itg2cnlem1  22337  itgfsum  22402  cnlimc  22461  dvlip2  22565  itgsubst  22619  plyeq0lem  22776  plypf1  22778  dvtaylp  22934  ulmcaulem  22958  ulmcau  22959  ulmcn  22963  ulmdvlem3  22966  mtest  22968  pserulm  22986  pserdvlem2  22992  logdivlt  23177  advlogexp  23207  cxpexp  23220  cxpcl  23226  xrlimcnp  23499  basellem4  23558  logexprlim  23701  dchrsum2  23744  sumdchr2  23746  rpvmasum2  23898  pntrsumbnd2  23953  pntleml  23997  tglineeltr  24215  brbtwn2  24413  colinearalglem4  24417  axeuclidlem  24470  axcontlem8  24479  axcontlem10  24481  clwwisshclww  25012  grpoidinvlem3  25409  grpoideu  25412  grpoinveu  25425  nmcvcn  25806  nmounbi  25892  blocnilem  25920  ubthlem1  25987  h2hlm  26098  ocsh  26402  brafnmul  27071  kbpj  27076  nmcexi  27146  lnconi  27153  riesz1  27185  mdbr2  27416  mdsl0  27430  mdslmd3i  27452  csmdsymi  27454  atcvatlem  27505  chirredlem1  27510  chirredi  27514  cdj3lem2b  27557  xrge0infss  27814  oduprs  27881  submarchi  27967  ordtrest2NEWlem  28142  voliune  28441  cvxscon  28955  noreson  29663  btwnouttr2  29903  cgrxfr  29936  btwnxfr  29937  lineext  29957  segcon2  29986  brsegle2  29990  seglecgr12im  29991  segletr  29995  broutsideof3  30007  outsideofeu  30012  lineunray  30028  lineelsb2  30029  fin2solem  30282  heicant  30292  mblfinlem3  30296  volsupnfl  30302  itg2addnclem  30309  itg2addnclem2  30310  itg2addnclem3  30311  ftc1anclem1  30333  ftc1anclem5  30337  ftc1anclem6  30338  ftc1anc  30341  neibastop3  30423  unirep  30446  filbcmb  30474  fzmul  30476  fdc  30481  nninfnub  30487  isbnd2  30522  bndss  30525  prdsbnd  30532  prdstotbnd  30533  ismtyres  30547  rrnmet  30568  rrncmslem  30571  rrnequiv  30574  ghomco  30588  grpokerinj  30590  rngonegmn1l  30595  isdrngo2  30604  rngoisocnv  30627  divrngidl  30668  intidl  30669  unichnidl  30671  prnc  30707  isfldidl  30708  mzpindd  30921  radcnvrat  31439  lcmgcdlem  31456  expgrowth  31484  fnchoice  31647  icccncfext  31932  dvnmul  31982  dvnprodlem2  31986  stoweidlem17  32041  stoweidlem30  32054  stoweidlem38  32062  stoweidlem42  32066  stoweidlem44  32068  fourierdlem31  32162  fourierdlem73  32204  fourierdlem74  32205  fourierdlem75  32206  fourierdlem83  32214  fourierdlem94  32225  fourierdlem113  32244  etransclem4  32263  mndpsuppss  33237  aacllem  33623  bnj110  34336  cvrexchlem  35559  ps-2  35618  3atnelvolN  35726  dib1dim  37308  dib1dim2  37311
  Copyright terms: Public domain W3C validator