ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  an4s Unicode version

Theorem an4s 560
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 558 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ( ph  /\  ps )  /\  ( ch  /\  th )
) )
2 an4s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
31, 2sylbi 120 1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an42s  561  anandis  564  anandirs  565  trin2  4898  fnun  5197  2elresin  5202  f1co  5308  f1oun  5353  f1oco  5356  f1mpt  5638  poxp  6095  tfrlem7  6180  brecop  6485  th3qlem1  6497  oviec  6501  pmss12g  6535  addcmpblnq  7139  mulcmpblnq  7140  mulpipqqs  7145  mulclnq  7148  mulcanenq  7157  distrnqg  7159  mulcmpblnq0  7216  mulcanenq0ec  7217  mulclnq0  7224  nqnq0a  7226  nqnq0m  7227  distrnq0  7231  genipv  7281  genpelvl  7284  genpelvu  7285  genpml  7289  genpmu  7290  genpcdl  7291  genpcuu  7292  genprndl  7293  genprndu  7294  distrlem1prl  7354  distrlem1pru  7355  ltsopr  7368  addcmpblnr  7511  ltsrprg  7519  addclsr  7525  mulclsr  7526  addasssrg  7528  addresr  7609  mulresr  7610  axaddass  7644  axmulass  7645  axdistr  7646  mulgt0  7803  mul4  7858  add4  7887  2addsub  7940  addsubeq4  7941  sub4  7971  muladd  8110  mulsub  8127  add20i  8218  mulge0i  8345  mulap0b  8379  divmuldivap  8435  ltmul12a  8578  zmulcl  9061  uz2mulcl  9354  qaddcl  9379  qmulcl  9381  qreccl  9386  rpaddcl  9416  ge0addcl  9715  ge0xaddcl  9717  expge1  10281  rexanuz  10711  amgm2  10841  iooinsup  10997  mulcn2  11032  dvds2ln  11433  opoe  11499  omoe  11500  opeo  11501  omeo  11502  lcmgcd  11666  lcmdvds  11667  tgcl  12139  innei  12238  txbas  12333  txss12  12341  txbasval  12342  blsscls2  12568  qtopbasss  12596  bj-indind  12964
  Copyright terms: Public domain W3C validator