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

Theorem 3comr 1172
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 1171 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1171 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 945
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 947
This theorem is referenced by:  nnacan  6374  le2tri3i  7836  ltaddsublt  8296  div12ap  8414  lemul12b  8576  zdivadd  9091  zdivmul  9092  elfz  9736  fzmmmeqm  9778  fzrev  9804  absdiflt  10804  absdifle  10805  dvds0lem  11399  dvdsmulc  11417  dvds2add  11423  dvds2sub  11424  dvdstr  11426  lcmdvds  11656  psmettri2  12392  xmettri2  12425
  Copyright terms: Public domain W3C validator