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

Theorem 3comr 1147
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3comr ((𝜒𝜑𝜓) → 𝜃)

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213coml 1146 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1146 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  nnacan  6151  le2tri3i  7286  ltaddsublt  7738  div12ap  7849  lemul12b  8006  zdivadd  8517  zdivmul  8518  elfz  9111  fzmmmeqm  9152  fzrev  9177  absdiflt  10116  absdifle  10117  dvds0lem  10350  dvdsmulc  10368  dvds2add  10374  dvds2sub  10375  dvdstr  10377  lcmdvds  10605
  Copyright terms: Public domain W3C validator