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

Theorem 3comr 1193
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 1192 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1192 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 963
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 965
This theorem is referenced by:  nnacan  6459  le2tri3i  7985  ltaddsublt  8446  div12ap  8567  lemul12b  8732  zdivadd  9253  zdivmul  9254  elfz  9918  fzmmmeqm  9960  fzrev  9986  absdiflt  10992  absdifle  10993  dvds0lem  11696  dvdsmulc  11714  dvds2add  11720  dvds2sub  11721  dvdstr  11723  lcmdvds  11955  psmettri2  12728  xmettri2  12761
  Copyright terms: Public domain W3C validator