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  4561  xpexr2m  5069  f1elima  5771  f1imaeq  5773  isosolem  5822  caovlem2d  6064  2ndconst  6220  isotilem  7002  prarloclem4  7494  mulsub  8354  leltadd  8400  eqord1  8436  divmul24ap  8669  fprodseq  11584  grpidpropdg  12725  cmnpropd  13029  unitpropdg  13248  blcomps  13767  blcom  13768  cxple  14208  cxple3  14212
  Copyright terms: Public domain W3C validator