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

Theorem 3comr 1154
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 1153 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1153 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  nnacan  6311  le2tri3i  7690  ltaddsublt  8145  div12ap  8258  lemul12b  8419  zdivadd  8934  zdivmul  8935  elfz  9579  fzmmmeqm  9621  fzrev  9647  absdiflt  10656  absdifle  10657  dvds0lem  11249  dvdsmulc  11267  dvds2add  11273  dvds2sub  11274  dvdstr  11276  lcmdvds  11504  psmettri2  12130  xmettri2  12163
  Copyright terms: Public domain W3C validator