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

Theorem an42s 531
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 530 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
32ancom2s 508 1  |-  ( ( ( ph  /\  ch )  /\  ( th  /\  ps ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  nnmsucr  6098  ecopoveq  6232  enqdc  6517  addcmpblnq  6523  addpipqqslem  6525  addpipqqs  6526  addclnq  6531  addcomnqg  6537  distrnqg  6543  recexnq  6546  ltdcnq  6553  ltexnqq  6564  enq0enq  6587  enq0sym  6588  enq0breq  6592  addclnq0  6607  distrnq0  6615  mulclsr  6897  axmulass  7005  axdistr  7006  subadd4  7318  mulsub  7470
  Copyright terms: Public domain W3C validator