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

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

Proof of Theorem an42s
StepHypRef Expression
1 an41r3s.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
21an4s 555 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
32ancom2s 533 1  |-  ( ( ( ph  /\  ch )  /\  ( th  /\  ps ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nnmsucr  6241  ecopoveq  6377  enqdc  6910  addcmpblnq  6916  addpipqqslem  6918  addpipqqs  6919  addclnq  6924  addcomnqg  6930  distrnqg  6936  recexnq  6939  ltdcnq  6946  ltexnqq  6957  enq0enq  6980  enq0sym  6981  enq0breq  6985  addclnq0  7000  distrnq0  7008  mulclsr  7290  axmulass  7398  axdistr  7399  subadd4  7716  mulsub  7869
  Copyright terms: Public domain W3C validator