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

Theorem ancom2s 566
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
an12s.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
ancom2s  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )

Proof of Theorem ancom2s
StepHypRef Expression
1 pm3.22 265 . 2  |-  ( ( ch  /\  ps )  ->  ( ps  /\  ch ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 286 1  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  an42s  589  ordsuc  4562  xpexr2m  5070  f1elima  5773  f1imaeq  5775  isosolem  5824  caovlem2d  6066  2ndconst  6222  isotilem  7004  prarloclem4  7496  mulsub  8357  leltadd  8403  eqord1  8439  divmul24ap  8672  fprodseq  11590  grpidpropdg  12792  cmnpropd  13096  unitpropdg  13315  blcomps  13866  blcom  13867  cxple  14307  cxple3  14311
  Copyright terms: Public domain W3C validator