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

Theorem an4s 800
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an4s.1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Assertion
Ref Expression
an4s  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )

Proof of Theorem an4s
StepHypRef Expression
1 an4 798 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ( ph  /\  ps )  /\  ( ch  /\  th )
) )
2 an4s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
31, 2sylbi 188 1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  an42s  801  anandis  804  anandirs  805  2mo  2332  frminex  4522  trin2  5216  fnun  5510  2elresin  5515  f1co  5607  f1oun  5653  f1oco  5657  f1mpt  5966  poxp  6417  soxp  6418  tfrlem2  6596  tfrlem5  6600  oeoe  6801  brecop  6956  th3qlem1  6969  ovec  6973  pmss12g  6999  dif1enOLD  7299  dif1en  7300  fiin  7385  tcmin  7636  harval2  7840  genpv  8832  genpdm  8835  genpnnp  8838  genpcd  8839  genpnmax  8840  addcmpblnr  8903  mulcmpblnr  8905  addsrpr  8906  mulsrpr  8907  ltsrpr  8908  addclsr  8914  mulclsr  8915  addasssr  8919  mulasssr  8921  distrsr  8922  mulgt0sr  8936  addresr  8969  mulresr  8970  axaddf  8976  axmulf  8977  axaddass  8987  axmulass  8988  axdistr  8989  mulgt0  9109  mul4  9191  add4  9237  2addsub  9275  addsubeq4  9276  sub4  9302  muladd  9422  mulsub  9432  mulge0  9501  mulge0OLD  9502  add20i  9526  mulge0i  9530  mulne0  9620  divmuldiv  9670  rec11i  9711  ltmul12a  9822  zmulcl  10280  uz2mulcl  10509  qaddcl  10546  qmulcl  10548  qreccl  10550  rpaddcl  10588  xmulgt0  10818  xmulge0  10819  ixxin  10889  ge0addcl  10965  ge0xaddcl  10967  fzm1  11082  serge0  11332  expge1  11372  sqrmo  12012  rexanuz  12104  amgm2  12128  mulcn2  12344  dvds2ln  12835  divalglem6  12873  divalglem8  12875  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pc2dvds  13207  catpropd  13890  spwmo  14613  gimco  15010  efgrelexlemb  15337  tgcl  16989  innei  17144  iunconlem  17443  txbas  17552  txss12  17590  txbasval  17591  tx1stc  17635  fbunfip  17854  tsmsxp  18137  blsscls2  18487  bddnghm  18713  qtopbaslem  18745  iimulcl  18915  icoopnst  18917  iocopnst  18918  iccpnfcnv  18922  pf1ind  19928  mumullem2  20916  fsumvma  20950  lgslem3  21035  pntrsumbnd2  21214  ajmoi  22313  hvadd4  22491  hvsub4  22492  shsel3  22770  shscli  22772  shscom  22774  chj4  22990  5oalem3  23111  5oalem5  23113  5oalem6  23114  hoadd4  23240  adjmo  23288  adjsym  23289  cnvadj  23348  leopmuli  23589  mdslmd1lem2  23782  chirredlem2  23847  chirredi  23850  cdjreui  23888  addltmulALT  23902  reofld  24233  xrge0iifcnv  24272  mulge0b  25144  poseq  25467  wfr3g  25469  wfrlem11  25480  frr3g  25494  frrlem4  25498  frrlem5c  25501  funtransport  25869  btwnconn1lem13  25937  btwnconn1lem14  25938  outsideofeu  25969  outsidele  25970  funray  25978  lineintmo  25995  itg2gt0cn  26159  fzadd2  26335  bndss  26385  isdrngo3  26465  riscer  26494  intidl  26529  psgnghm  27305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator