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

Theorem 3comr 1201
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 1200 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1200 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 970
This theorem is referenced by:  nnacan  6480  le2tri3i  8007  ltaddsublt  8469  div12ap  8590  lemul12b  8756  zdivadd  9280  zdivmul  9281  elfz  9950  fzmmmeqm  9993  fzrev  10019  absdiflt  11034  absdifle  11035  dvds0lem  11741  dvdsmulc  11759  dvds2add  11765  dvds2sub  11766  dvdstr  11768  lcmdvds  12011  psmettri2  12968  xmettri2  13001
  Copyright terms: Public domain W3C validator