ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3coml Structured version   GIF version

Theorem 3coml 1110
Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3coml ((ψ χ φ) → θ)

Proof of Theorem 3coml
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213com23 1109 . 2 ((φ χ ψ) → θ)
323com13 1108 1 ((ψ χ φ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3comr  1111  nndir  6008  f1oen2g  6171  f1dom2g  6172  addassnqg  6366  ltbtwnnqq  6398  nnanq0  6440  ltasrg  6678  recexgt0sr  6681  axmulass  6737  adddir  6796  axltadd  6866  ltleletr  6877  letr  6878  pnpcan2  7027  subdir  7159  div13ap  7434  zdiv  8084  xrletr  8474  fzen  8657  fzrevral2  8718  fzshftral  8720  fzind2  8845
  Copyright terms: Public domain W3C validator