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 369
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 371
This theorem is referenced by:  anass1rs  805  anabss1  810  wereu2  4826  ordintdif  4877  ordunisssuc  4930  sossfld  5394  fssres  5687  foco  5739  dffv2  5874  fconstfv  6050  isocnv  6131  f1oiso  6152  f1ocnvfv3  6197  fun11iun  6648  onfununi  6913  oev2  7074  oaordi  7096  oaass  7111  omlimcl  7128  odi  7129  omass  7130  oewordri  7142  oelim2  7145  oeoa  7147  oeoe  7149  nnaordi  7168  omabs  7197  eceqoveq  7316  mapxpen  7588  mapdom2  7593  dif1enOLD  7656  dif1en  7657  findcard  7663  fimax2g  7670  isfinite2  7682  rankval3b  8145  isf32lem9  8642  fin1a2s  8695  zornn0g  8786  gchen1  8904  gchen2  8905  intwun  9014  suplem2pr  9334  recexsrlem  9382  axpre-sup  9448  axsup  9562  dedekind  9645  recextlem2  10079  divne0  10118  dfinfmr  10419  uzindOLD  10848  qreccl  11085  xrlttr  11229  xaddf  11306  xrsupsslem  11381  xrinfmsslem  11382  supxr2  11388  supxrunb1  11394  supxrbnd1  11396  supxrbnd2  11397  modid  11850  seqof  11981  cau3lem  12961  lo1bdd2  13121  o1co  13183  rlimcn2  13187  climcn1  13188  climcn2  13189  rlimsqzlem  13245  caucvgb  13276  fsumrlim  13393  fsumo1  13394  rplpwr  13859  dvdssq  13863  nn0seqcvgd  13864  isprm2lem  13889  isprm6  13914  phiprmpw  13970  pcneg  14059  prmpwdvds  14084  4sqlem19  14143  0ramcl  14203  imasleval  14599  catpropd  14768  funcres2c  14931  acsfiindd  15467  latdisdlem  15479  dirtr  15526  mrcmndind  15614  grpinveu  15692  mulgnn0subcl  15760  mulgsubcl  15761  mhmmulg  15779  cycsubgcl  15827  cycsubgss  15828  ghmmulg  15879  odf1  16185  dfod2  16187  gexdvds2  16206  sylow2blem3  16243  frgpup1  16394  iscyggen2  16480  iscyg3  16485  prdsgsum  16594  prdsgsumOLD  16595  rngrghm  16818  dvdsrcl2  16866  crngunit  16878  dvdsrpropd  16912  lss1d  17168  divscrng  17446  coe1tmmul  17855  mulgghm2  18051  mulgghm2OLD  18054  frgpcyg  18132  ip0r  18192  isphld  18209  frlmgsumOLD  18321  frlmgsum  18322  uvcresum  18344  mdetdiagid  18539  tgcl  18707  0ntr  18808  innei  18862  neitr  18917  ordtrest2lem  18940  cncnp  19017  cnnei  19019  2ndcdisj  19193  dislly  19234  kgenss  19249  ptcnplem  19327  ptcnp  19328  ptcn  19333  cnmpt2k  19394  qtoprest  19423  kqt0lem  19442  isr0  19443  kqreglem1  19447  trfilss  19595  isufil2  19614  ufileu  19625  hausflim  19687  cnextcn  19772  symgtgp  19805  tsmssubm  19849  tsmsxplem1  19860  ustfilxp  19920  ustuqtop0  19948  elbl2ps  20097  elbl2  20098  nrginvrcn  20405  nmoix  20441  nmoleub  20443  cncfco  20616  icccvx  20655  iscmet3  20937  rrxmet  21040  ovolfioo  21084  ovolficc  21085  ovolicc2lem4  21136  iunmbl2  21172  dyadmax  21212  mbfsup  21276  mbflimsup  21278  mbflim  21280  itg1addlem4  21311  mbfi1flimlem  21334  itg2monolem1  21362  itg2mono  21365  itg2i1fseqle  21366  itg2i1fseq  21367  itg2addlem  21370  itg2gt0  21372  itg2cnlem1  21373  itgfsum  21438  cnlimc  21497  dvlip2  21601  itgsubst  21655  plyeq0lem  21812  plypf1  21814  dvtaylp  21969  ulmcaulem  21993  ulmcau  21994  ulmcn  21998  ulmdvlem3  22001  mtest  22003  pserulm  22021  pserdvlem2  22027  logdivlt  22204  advlogexp  22234  cxpexp  22247  cxpcl  22253  xrlimcnp  22496  basellem4  22555  logexprlim  22698  dchrsum2  22741  sumdchr2  22743  rpvmasum2  22895  pntrsumbnd2  22950  pntleml  22994  tglineeltr  23177  brbtwn2  23304  colinearalglem4  23308  axeuclidlem  23361  axcontlem8  23370  axcontlem10  23372  grpoidinvlem3  23846  grpoideu  23849  grpoinveu  23862  nmcvcn  24243  nmounbi  24329  blocnilem  24357  ubthlem1  24424  h2hlm  24535  ocsh  24839  brafnmul  25508  kbpj  25513  nmcexi  25583  lnconi  25590  riesz1  25622  mdbr2  25853  mdsl0  25867  mdslmd3i  25889  csmdsymi  25891  atcvatlem  25942  chirredlem1  25947  chirredi  25951  cdj3lem2b  25994  xrge0infss  26205  oduprs  26263  submarchi  26349  ordtrest2NEWlem  26498  voliune  26790  cvxscon  27277  ntrivcvg  27557  noreson  27946  btwnouttr2  28198  cgrxfr  28231  btwnxfr  28232  lineext  28252  segcon2  28281  brsegle2  28285  seglecgr12im  28286  segletr  28290  broutsideof3  28302  outsideofeu  28307  lineunray  28323  lineelsb2  28324  fin2solem  28564  heicant  28575  mblfinlem3  28579  volsupnfl  28585  itg2addnclem  28592  itg2addnclem2  28593  itg2addnclem3  28594  ftc1anclem1  28616  ftc1anclem5  28620  ftc1anclem6  28621  ftc1anc  28624  neibastop3  28732  unirep  28755  filbcmb  28783  fzmul  28785  fdc  28790  nninfnub  28796  isbnd2  28831  bndss  28834  prdsbnd  28841  prdstotbnd  28842  ismtyres  28856  rrnmet  28877  rrncmslem  28880  rrnequiv  28883  ghomco  28897  grpokerinj  28899  rngonegmn1l  28904  isdrngo2  28913  rngoisocnv  28936  divrngidl  28977  intidl  28978  unichnidl  28980  prnc  29016  isfldidl  29017  mzpindd  29231  expgrowth  29758  fnchoice  29900  stoweidlem17  29961  stoweidlem30  29974  stoweidlem38  29982  stoweidlem42  29986  stoweidlem44  29988  clwwisshclww  30620  mndpsuppss  30933  cpmatmcllem  31208  bnj110  32184  cvrexchlem  33402  ps-2  33461  3atnelvolN  33569  dib1dim  35149  dib1dim2  35152
  Copyright terms: Public domain W3C validator