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  6441  ltasrg  6698  recexgt0sr  6701  axmulass  6757  adddir  6816  axltadd  6886  ltleletr  6897  letr  6898  pnpcan2  7047  subdir  7179  div13ap  7454  zdiv  8104  xrletr  8494  fzen  8677  fzrevral2  8738  fzshftral  8740  fzind2  8865
  Copyright terms: Public domain W3C validator