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

Theorem 3comr 1206
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 1205 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1205 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 973
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 975
This theorem is referenced by:  nnacan  6491  le2tri3i  8028  ltaddsublt  8490  div12ap  8611  lemul12b  8777  zdivadd  9301  zdivmul  9302  elfz  9971  fzmmmeqm  10014  fzrev  10040  absdiflt  11056  absdifle  11057  dvds0lem  11763  dvdsmulc  11781  dvds2add  11787  dvds2sub  11788  dvdstr  11790  lcmdvds  12033  psmettri2  13122  xmettri2  13155
  Copyright terms: Public domain W3C validator