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

Theorem an4s 562
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 560 . 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  563  anandis  566  anandirs  567  trin2  4900  fnun  5199  2elresin  5204  f1co  5310  f1oun  5355  f1oco  5358  f1mpt  5640  poxp  6097  tfrlem7  6182  brecop  6487  th3qlem1  6499  oviec  6503  pmss12g  6537  addcmpblnq  7143  mulcmpblnq  7144  mulpipqqs  7149  mulclnq  7152  mulcanenq  7161  distrnqg  7163  mulcmpblnq0  7220  mulcanenq0ec  7221  mulclnq0  7228  nqnq0a  7230  nqnq0m  7231  distrnq0  7235  genipv  7285  genpelvl  7288  genpelvu  7289  genpml  7293  genpmu  7294  genpcdl  7295  genpcuu  7296  genprndl  7297  genprndu  7298  distrlem1prl  7358  distrlem1pru  7359  ltsopr  7372  addcmpblnr  7515  ltsrprg  7523  addclsr  7529  mulclsr  7530  addasssrg  7532  addresr  7613  mulresr  7614  axaddass  7648  axmulass  7649  axdistr  7650  mulgt0  7807  mul4  7862  add4  7891  2addsub  7944  addsubeq4  7945  sub4  7975  muladd  8114  mulsub  8131  add20i  8222  mulge0i  8350  mulap0b  8384  divmuldivap  8440  ltmul12a  8586  zmulcl  9075  uz2mulcl  9370  qaddcl  9395  qmulcl  9397  qreccl  9402  rpaddcl  9433  ge0addcl  9732  ge0xaddcl  9734  expge1  10298  rexanuz  10728  amgm2  10858  iooinsup  11014  mulcn2  11049  dvds2ln  11453  opoe  11519  omoe  11520  opeo  11521  omeo  11522  lcmgcd  11686  lcmdvds  11687  tgcl  12160  innei  12259  txbas  12354  txss12  12362  txbasval  12363  blsscls2  12589  qtopbasss  12617  bj-indind  13057
  Copyright terms: Public domain W3C validator