ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancom2s GIF 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 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
ancom2s ((𝜑 ∧ (𝜒𝜓)) → 𝜃)

Proof of Theorem ancom2s
StepHypRef Expression
1 pm3.22 265 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 286 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
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  4580  xpexr2m  5088  f1elima  5795  f1imaeq  5797  isosolem  5846  caovlem2d  6090  2ndconst  6248  isotilem  7036  prarloclem4  7528  mulsub  8389  leltadd  8435  eqord1  8471  divmul24ap  8704  fprodseq  11626  grpidpropdg  12853  cmnpropd  13251  unitpropdg  13515  blcomps  14373  blcom  14374  cxple  14814  cxple3  14818
  Copyright terms: Public domain W3C validator