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

Theorem 3comr 1212
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 1211 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1211 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  nnacan  6527  le2tri3i  8080  ltaddsublt  8542  div12ap  8665  lemul12b  8832  zdivadd  9356  zdivmul  9357  elfz  10028  fzmmmeqm  10072  fzrev  10098  absdiflt  11115  absdifle  11116  dvds0lem  11822  dvdsmulc  11840  dvds2add  11846  dvds2sub  11847  dvdstr  11849  lcmdvds  12093  psmettri2  14181  xmettri2  14214
  Copyright terms: Public domain W3C validator